Computer Science ›› 2014, Vol. 41 ›› Issue (8): 42-46.doi: 10.11896/j.issn.1002-137X.2014.08.008

Previous Articles     Next Articles

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

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!
Full text



[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75, 88 .
[2] XIA Qing-xun and ZHUANG Yi. Remote Attestation Mechanism Based on Locality Principle[J]. Computer Science, 2018, 45(4): 148 -151, 162 .
[3] LI Bai-shen, LI Ling-zhi, SUN Yong and ZHU Yan-qin. Intranet Defense Algorithm Based on Pseudo Boosting Decision Tree[J]. Computer Science, 2018, 45(4): 157 -162 .
[4] WANG Huan, ZHANG Yun-feng and ZHANG Yan. Rapid Decision Method for Repairing Sequence Based on CFDs[J]. Computer Science, 2018, 45(3): 311 -316 .
[5] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[6] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[7] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[8] LIU Qin. Study on Data Quality Based on Constraint in Computer Forensics[J]. Computer Science, 2018, 45(4): 169 -172 .
[9] ZHONG Fei and YANG Bin. License Plate Detection Based on Principal Component Analysis Network[J]. Computer Science, 2018, 45(3): 268 -273 .
[10] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99, 116 .