Top

Published in:

2019 | OriginalPaper | Chapter

Embedding CCSL into Dynamic Logic: A Logical Approach for the Verification of CCSL Specifications

Authors : Yuanrui Zhang, Hengyang Wu, Yixiang Chen, Frédéric Mallet

Published in: Formal Techniques for Safety-Critical Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

The Clock Constraint Specification Language (CCSL) is a clock-based specification language for capturing causal and chronometric constraints between events in Real-Time Embedded Systems (RTESs). Due to the limitations of the existing verification approaches, CCSL lacks a full verification support for ‘unsafe CCSL specifications’ and a unified proof framework. In this paper, we propose a novel verification approach based on theorem proving and SMT-checking. We firstly build a logic called CCSL Dynamic Logic (CDL), which extends the traditional dynamic logic with ‘signals’ and ‘clock relations’ as primitives, and with synchronous execution mechanism for modelling RTESs. Then we propose a sound and relatively complete proof system for CDL to provide the verification support. We show how CDL can be used to capture RTES and verify CCSL specifications by analyzing a simple case study.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Formal Timing Analysis of Digital Circuits

next chapter Refinement of Statecharts with Run-to-Completion Semantics

In SEP, for convenience, we use the same name ‘c’ to represent the signal corresponding to clock c, which should not cause any ambiguities. Sometimes we also say a signal c in p ‘a clock c in p’.

OMG: UML profile for MARTE: Modeling and analysis of real-time embedded systems. Technical report, OMG, June 2011. Formal 02 June 2011

Mallet, F.: Clock constraint specification language: specifying clock constraints with UML/MARTE. ISSE 4(3), 309–314 (2008)

André, C.: Syntax and semantics of the clock constraint specification language (CCSL). Research Report RR-6925, INRIA (2009)

Mallet, F., de Simone, R.: Correctness issues on MARTE/CCSL constraints. Sci. Comput. Program. 106, 78–92 (2015)CrossRef

Mallet, F., Millo, J.V., de Simone, R.: Safe CCSL specifications and marked graphs. In: 11th ACM/IEEE International Conference on Formal Methods and Models for Codesign, pp. 157–166, IEEE (2013)

Zhang, M., Ying, Y.: Towards SMT-based LTL model checking of clock constraint specification language for real-time and embedded systems. In: LCTES 2017, pp. 61–70. ACM (2017)CrossRef

Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. SIGACT News 32(1), 66–69 (2001)CrossRef

Harel, D. (ed.): First-Order Dynamic Logic. LNCS, vol. 68. Springer, Heidelberg (1979). https://doi.org/10.1007/3-540-09237-4CrossRefMATH

Halbwachs, N.: Synchronous Programming of Reactive Systems. Kluwer Academic Publisher, Dordrecht (1993)CrossRef

10.

Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org

11.

Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL—A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9CrossRefMATH

12.

Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5CrossRefMATH

13.

Zhang, M., Mallet, F., Zhu, H.: An SMT-based approach to the formal analysis of MARTE/CCSL. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 433–449. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47846-3_27CrossRef

14.

Berry, G., Gonthier, G.: The Esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87–152 (1992)CrossRef

15.

Gentzen, G.: Untersuchungen über das logische Schließen. Ph.D. thesis, NA, Göttingen (1934)

16.

Platzer, A.: Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14509-4CrossRefMATH

17.

André, C., Mallet, F.: Specification and verification of time requirements with CCSL and Esterel. In: LCTES 2009, pp. 167–176. ACM (2009)

18.

Suryadevara, J., Seceleanu, C., Mallet, F., Pettersson, P.: Verifying MARTE/CCSL mode behaviors using UPPAAL. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 1–15. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40561-7_1CrossRef

19.

Zhang, Y., Mallet, F., Chen, Y.: Timed automata semantics of spatio-temporal consistency language STeC. In: TASE 2014, pp. 201–208, IEEE (2014)

20.

Zhang, M., Dai, F., Mallet, F.: Periodic scheduling for MARTE/CCSL: theory and practice. Sci. Comput. Program. 154, 42–60 (2018)CrossRef

21.

Platzer, A.: A temporal dynamic logic for verifying hybrid system invariants. In: Artemov, S.N., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 457–471. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72734-7_32CrossRef

Title: Embedding CCSL into Dynamic Logic: A Logical Approach for the Verification of CCSL Specifications
Authors: Yuanrui Zhang
Hengyang Wu
Yixiang Chen
Frédéric Mallet
Publisher: Springer International Publishing
Book: Formal Techniques for Safety-Critical Systems
Print ISBN: 978-3-030-12987-3

Electronic ISBN: 978-3-030-12988-0

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-12988-0_7

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner