Combining CCSL and Esterel to specify and verify time requirements
Explore this paper's citation graph
Summary
The formal semantics of C CSL clock constraints are introduced and a process to use CCSL both as a high-level specification language for UML models and as a golden model to verify the conformance of implementations is proposed.
- Type
- article
- Published
- 2009-01-01
- Cited by
- 9
- References
- 40
- Access
- Open access
- OpenAlex
- https://openalex.org/W45469007
- Semantic Scholar
- https://api.semanticscholar.org/CorpusID:14193745
Keywords
Computer science, Programming language, Context (archaeology), Concurrency
References
- Systems engineering with SysML / UML - modeling, analysis, design
- Representation and Analysis of Reactive Behaviors: A Synchronous Approach
- The foundations of Esterel
- Modeling statecharts and activitycharts as signal equations
- Computing SyncCharts Reactions
- Synchronous Programming with Events and Relations: the SIGNAL Language and Its Semantics
- A discrete-time UML semantics for concurrency and communication in safety-critical applications
- On the Semantics of UML/MARTE Clock Constraints
- Petri Nets
- A framework for comparing models of computation
- The synchronous languages 12 years later
- Simulation of Multi-Formalism Models with ModHel'X
- N-synchronous Kahn networks: a relaxed model of synchrony for real-time systems
- Semantics and Verification of Data Flow in UML 2.0 Activities
- Taming heterogeneity - the Ptolemy approach
- Compiling Esterel
- Time, clocks, and the ordering of events in a distributed system
- Constraints
- Interpolation and SAT-Based Model Checking
- Concurrency theory
Cited by
- A real-time architecture design language for multi-rate embedded control systems
- Executing AADL Models with UML/MARTE
- A Synchronous Language for Critical Embedded Systems with Multiple Real-Time Constraints. (Un Langage Synchrone pour les Systèmes Embarqués Critiques Soumis à des Contraintes Temps Réel Multiples)
- Syntax and Semantics of the Clock Constraint Specification Language (CCSL)
- On the Formal Execution of UML and DSL Models
- Verifying end-to-end real-time constraints on multi-periodic models
- Un langage synchrone pour les systèmes embarqués critiques soumis à des contraintes temps réel multiples
- Theme : Embedded and Real Time Systems Project-team Aoste Models and Methods for the Analysis and Optimization of Systems with Real-time and Embedded Constraints
- Instant-Based and State-Based Analysis of Infinite Logical Clock
- Syntax and Semantics of the Clock Constraint Speci cation Language ( CCSL )
Related papers
- Verification of clock constraints: CCSL Observers in Esterel
- Specification and verification of time requirements with CCSL and Esterel
- A dynamic assertion-based verification platform for UML statecharts over rhapsody
- Formal methods and software engineering : 4th International Conference on Formal Engineering Methods, ICFEM 2002, Shanghai, China, October 21-25, 2002 : proceedings
- Compiling Modechart specifications
- Extended timing diagrams as a specification language
- Fundamental approaches to software engineering : 4th International Conference, FASE 2001, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2-6, 2001 : proceedings
- Time assignment for distributed service and protocol UML-based specifications