微信服务号

微信订阅号

2025-4-6- 6
Home > Archive>Volume 29, Issue 6, 2018 >1595-1606. DOI:10.13328/j.cnki.jos.005469
PDF HTML XML Export Cite reminder
SMT-Based Approach to Formal Analysis of CCSL with Tool Support
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61502171)

  • Article
    • | |
  • Metrics
    • |
  • Reference [24]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    CCSL (abbreviated for clock constraint specification language) is a formal language for specifying the constraints on the occurrences of events in real-time and embedded systems. CCSL is a companion language of MARTE (abbreviated for modeling and analysis of real-time and embedded systems), a UML profile which provides support for specification, design, and verification/validation stages for model-driven development of real time and embedded Systems. Given a set of CCSL constraints, it is necessary to check if there exist schedules that satisfy all the constraints and if all the behaviors that conforming to the constraints will never incur deadlock of systems. Many approaches have been proposed based on state transition system, timed automata, etc. However, most of the existing approaches have some drawbacks, such as being ad hoc to specific formal analysis, and being suited to only subsets of CCSL constraints or inefficient. In this paper, a unified and efficient SMT-based approach to formal analysis of CCSL is proposed. This approach is unified in that it can be applied to various analysis such as validity proving, trace analysis, deadlock detection and LTL model checking. A prototype tool for the new approach is implemented to support the four types of formal analysis, utilizing the state-of-the-art SMT solvers such as Z3 and CVC4. With efficient SMT solvers, verification can be completed in a reasonable time, as demonstrated by the experimental results in the case studies.

    Reference
    [1] Object Management Group. UML profile for MARTE:Modeling and analysis of real-timeembedded systems. 2011.
    [2] André C. Syntax and semantics of the clock constraint specification language (CCSL). Research Report, RR-6925, INRIA, 2009.
    [3] Mallet F, André C. On the semantics of UML/MARTE clock constraints. In:Proc. of the IEEE Int'l Symp. on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC 2009). IEEE, 2009. 305-312.[doi:10.1109/ISORC.2009.27]
    [4] Kang EY, Schobbens PY. Schedulability analysis support for automotive systems:From requirement to implementation. In:Proc. of the 29th Annual ACM Symp. on Applied Computing. ACM Press, 2014. 1080-1085.[doi:10.1145/2554850.2554929]
    [5] Mallet F. MARTE/CCSL for modeling cyber-physical systems. In:Proc. of the Formal Modeling and Verification of CyberPhysical Systems. Springer Fachmedien Wiesbaden, 2015. 26-49.[doi:10.1007/978-3-658-09994-7_2]
    [6] Mallet F, De Simone R. Correctness issues on MARTE/CCSL constraints. Science of Computer Programming, 2015,106:78-92.[doi:10.1016/j.scico.2015.03.001]
    [7] Yin L, Mallet F, Liu J. Verification of MARTE/CCSL time requirements in Promela/SPIN. In:Proc. of the 201116th IEEE Int'l Conf. on Engineering of Complex Computer Systems (ICECCS). IEEE, 2011. 65-74.[doi:10.1109/ICECCS.2011.14]
    [8] Gascon R, Mallet F, Deantoni J. Logical time and temporal logics:Comparing UML MARTE/CCSL and PSL. In:Proc. of the 201118th Int'l Symp. on Temporal Representation and Reasoning (TIME). IEEE, 2011. 141-148.[doi:10.1109/TIME.2011.10]
    [9] Suryadevara J, Seceleanu C, Mallet F, et al. Verifying MARTE/CCSL mode behaviors using UPPAAL. In:Proc. of the Int'l Conf. on Software Engineering and Formal Methods. Berlin, Heidelberg:Springer-Verlag, 2013. 1-15.[doi:10.1007/978-3-642-40561-7_1]
    [10] Zhang M, Mallet F. An executable semantics of clock constraint specification language and its applications. In:Proc. of the Int'l Workshop on Formal Techniques for Safety-Critical Systems. Cham:Springer-Verlag, 2015. 37-51.[doi:10.1007/978-3-319-29510-72]
    [11] Zhang M, Mallet F, Zhu H. An SMT-based approach to the formal analysis of MARTE/CCSL. In:Proc. of the Int'l Conf. on Formal Engineering Methods. Springer Int'l Publishing, 2016. 433-449.[doi:10.1007/978-3-319-47846-3_27]
    [12] Barrett C, Stump A, Tinelli C. The smt-lib standard:Version 2.0. In:Proc. of the 8th Int'l Workshop on Satisfiability Modulo Theories. Edinburgh, 2010. 13-14.
    [13] De Moura L, Bjørner N. Z3:An efficient SMT solver. In:Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. 2008. 337-340.[doi:10.1007/978-3-540-78800-3_24]
    [14] Cohen B, Venkataramanan S, Kumari A. System Verilog Assertions Handbook-For Formal and Dynamic Verification. Vhdlcohen Publishing, 2005.
    [15] Biere A, Cimatti A, Clarke EM, et al. Bounded model checking. Advances in Computers, 2003,58:117-148.
    [16] Cimatti A, Pistore M, Roveri M, et al. Improving the encoding of LTL model checking into SAT. In:Proc. of the Int'l Workshop on Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg:Springer-Verlag, 2002. 196-207.[doi:10.1007/3-540-47813-2_14]
    [17] Zhang W. SAT-Based verification of LTL formulas. In:Proc. of the FMICS/PDMC. 2006. 277-292.[doi:10.1007/978-3-540-70952-7_18]
    [18] Yu H, Talpin JP, Besnard L, et al. Polychronous controller synthesis from MARTE CCSL timing specifications. In:Proc. of the 9th ACM/IEEE Int'l Conf. on Formal Methods and Models for Codesign. IEEE Computer Society, 2011. 21-30.[doi:10.1109/MEMCOD.2011.5970507]
    [19] Zhang M, Ying Y. Towards SMT-based LTL model checking of clock constraint specification language for real-time and embedded systems. In:Proc. of the 18th ACM SIGPLAN/SIGBED Conf. on Languages, Compilers, and Tools for Embedded Systems. ACM Press, 2017. 61-70.[doi:10.1145/3078633.3081035]
    [20] Zhang M, Dai F, Mallet F. Periodic scheduling for MARTE/CCSL:Theory and practice. In:Proc. of the Science of Computer Programming. 2017.[doi:10.1016/j.scico.2017.08.015]
    [21] De Moura L, Owre S, Rueß H, et al. SAL 2. In:Proc. of the Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg:Springer-Verlag, 2004. 496-500.[doi:10.1007/978-3-540-27813-9_45]
    [22] Jin JW, Ma FF, Zhang J. Brief Introduction to SMT solving. Journal of Frontiers of Computer Science and Technology, 2015,9(7):769-780(in Chinese with English abstract).
    附中文参考文献:
    [22] 金继伟,马菲菲,张健.SMT求解技术简述.计算机科学与探索,2015,9(7):769-780.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

应云辉,张民.基于SMT的时钟约束语言CCSL的形式化分析方法与工具.软件学报,2018,29(6):1595-1606

Copy
Share
Article Metrics
  • Abstract:4246
  • PDF: 6445
  • HTML: 3149
  • Cited by: 0
History
  • Received:July 01,2017
  • Revised:September 01,2017
  • Adopted:November 06,2017
  • Online: December 28,2017
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063