计算机科学 ›› 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   
No Suggested Reading articles found!