计算机科学 ›› 2014, Vol. 41 ›› Issue (8): 42-46.doi: 10.11896/j.issn.1002-137X.2014.08.008

• 2013年全国理论计算机科学学术年会 • 上一篇    下一篇

基于层次化时间STM软件设计的形式化验证

周宽久,任龙涛,王小龙,勇嘉伟,侯刚   

  1. 大连理工大学软件学院 大连116620;大连理工大学软件评测中心 大连116620;大连理工大学软件学院 大连116620;大连理工大学软件学院 大连116620;大连理工大学软件学院 大连116620;大连理工大学软件学院 大连116620
  • 出版日期:2018-11-14 发布日期:2018-11-14
  • 基金资助:
    本文受国家自然科学基金(61272174)资助

Modeling and Formal Verification for Software Designs Based on Hierarchical Timed State Transition Matrix

ZHOU Kuan-jiu,REN Long-tao,WANG Xiao-long,YONG Jia-wei and HOU Gang   

  • Online:2018-11-14 Published:2018-11-14

摘要: 状态迁移矩阵(State Transition Matrix,STM)是一种基于表结构的程序建模语言。事件变量类型单一,事件和状态数量的增加很容易造成状态空间爆炸问题,无法表达具有时间语义的软件系统等原因,极大限制了该建模方法的推广应用。文中针对这些问题,首先提出层次化时间状态迁移矩阵(Hierarchical Time State Transition Matrix,HTSTM)模型,用于 设计、建模和验证 具有时间条件约束的软件系统,并给出形式化表示方法。基于该表示方法提出一种符号化编码方法,采用有界模型检测思想将需要验证的LTL性质输入SMT(Satisfiability Modulo Theories)求解器进行验证,从而在一定程度上证明了软件设计的正确性。

关键词: 层次化时间状态迁移矩阵,形式化验证,有界模型检测

Abstract: State Transition Matrix (STM) is a table-based modeling language.The popularization and application of this modeling method are greatly limited by the singleness of its event variable type,the state space explosion problem caused by the increasing events and states,and the weak expressive power in time semantics of software systems.We firstly presented a concept of Hierarchical Timed State Transition Matrix (HTSTM) which is mainly used for design,modeling and verification of software systems with time constraints.Then a formalization of HTSTM designs was pro-vided as a state transition system.Based on the formalization,we proposed a symbolic encoding approach which adopts the idea of Bounded Model Checking (BMC).Finally the LTL properties to be verified were determined by Satisfiability Modulo Theories (SMT) so that the correctness of the software design was proved to a certain extent.

Key words: Hierarchical time state transition matrix,Formal verification,Bounded model checking

[1] Matsumoto M,Anada K,Ueshima D,et al.Model Checking ofState Transition Matrix[R].ITSSV 2005,AIST Technical Report.2005:2-11
[2] Watanabe M.Extended Hierarchy State Transition Matrix Design Method -Version 2.0[R].CATS Technical Report.1998
[3] Clarke E,Kroening D,Ouaknine J,et al.Completeness and complexity of bounded model checking[C]∥Proceedings of the Ve-rification,Model Checking,and Abstract Interpretation.Springer Berlin Heidelberg,2004:85-96
[4] Clarke E M,Grumberg O,Peled D.Model checking[M].The MIT press,1999
[5] Armando A,Mantovani J,Platania L.Bounded model checking of software using SMT solvers instead of SAT solvers[M]∥Model Checking Software.Springer Berlin Heidelberg,2006:146-162
[6] Kong Wei-qiang,Fukuda A,Watanabe M.An SMT approach tobounded model checking of design in state transition matrix[C]∥Proceedings of the Computational Science and Its Applications (ICCSA).2010:231-238
[7] Kong Wei-qiang,Katahira N,Watanabe,et al.Formal verification of software designs in hierarchical state transition matrix with SMT-based bounded model checking[C]∥Proceedings of the Software Engineering Conference (APSEC).2011:81-88
[8] Latvala T,Biere A,Heljanko K,et al.Simple bounded LTLmodel checking[C]∥Proceedings of the Formal Methods in Computer-Aided Design-2004.2004:186-200
[9] Jussila T,Dubrovin J,Junttila T,et al.Model checking dynamic and hierarchical UML state machines[C]∥Proc.MoDeV2a:Model Development,Validation and Verification.2006:94-110
[10] Dubrovin J,Junttila T.Symbolic model checking of hierarchical UML state machines[C]∥Proceedings of the Application of Concurrency to System Design.2008:108-117
[11] Biere A,Cimatti A,Clarke EM,et al.Symbolic Model Checking without BDDs[C]∥TACAS 1999.1999:193-207
[12] Latvala T,Biere A,Heljanko K,et al.Simple is better:Efficient bounded model checking for past LTL[C]∥Proceedings of the Verification,Model Checking,and Abstract Interpretation.2005:380-395
[13] Lee E A,Seshia S A.Introduction to embedded systems:A cyber-physical systems approach[M].Lee & Seshia,2011
[14] Barrett C,Sebastiani R,Seshia S A,et al.Satisfiability modulo theories[J].Handbook of Satisfiability,2009,185:825-885
[15] Veanes M,Bjrner N,Alexander R.An SMT approach tobounded reachability analysis of model programs[C]∥Procee-dings of the Formal Techniques for Networked and Distributed Systems-FORTE 2008.Springer Berlin Heidelberg,2008:53-68
[16] 曾锃,赵建华.基于程序分析的代码查询技术[J].计算机科学,2012,9(2):143-147
[17] 何炎祥,吴伟,陈勇,等.基于 SMT 求解器的路径敏感程序验证[J].软件学报,2012,23(10)
[18] Dubrovin J,Junttila T,Heljanko K.Symbolic step encodings for object based communicating state machines[M].Springer Berlin Heidelberg,2008:96-112
[19] Cousot P.Abstract interpretation based formal methods and fu-ture challenges[C]∥Proceedings of the Informatics.2001:138-156
[20] De Moura L,Bjrner N.Z3:An efficient SMT solver[M]∥Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2008:337-340

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] 雷丽晖,王静. 可能性测度下的LTL模型检测并行化研究[J]. 计算机科学, 2018, 45(4): 71 -75 .
[2] 孙启,金燕,何琨,徐凌轩. 用于求解混合车辆路径问题的混合进化算法[J]. 计算机科学, 2018, 45(4): 76 -82 .
[3] 张佳男,肖鸣宇. 带权混合支配问题的近似算法研究[J]. 计算机科学, 2018, 45(4): 83 -88 .
[4] 伍建辉,黄中祥,李武,吴健辉,彭鑫,张生. 城市道路建设时序决策的鲁棒优化[J]. 计算机科学, 2018, 45(4): 89 -93 .
[5] 史雯隽,武继刚,罗裕春. 针对移动云计算任务迁移的快速高效调度算法[J]. 计算机科学, 2018, 45(4): 94 -99 .
[6] 周燕萍,业巧林. 基于L1-范数距离的最小二乘对支持向量机[J]. 计算机科学, 2018, 45(4): 100 -105 .
[7] 刘博艺,唐湘滟,程杰仁. 基于多生长时期模板匹配的玉米螟识别方法[J]. 计算机科学, 2018, 45(4): 106 -111 .
[8] 耿海军,施新刚,王之梁,尹霞,尹少平. 基于有向无环图的互联网域内节能路由算法[J]. 计算机科学, 2018, 45(4): 112 -116 .
[9] 崔琼,李建华,王宏,南明莉. 基于节点修复的网络化指挥信息系统弹性分析模型[J]. 计算机科学, 2018, 45(4): 117 -121 .
[10] 王振朝,侯欢欢,连蕊. 抑制CMT中乱序程度的路径优化方案[J]. 计算机科学, 2018, 45(4): 122 -125 .