Abstract
Many of the timing constraints expressed in physical prescriptions of distributed systems and multi-clock electronic systems can be expressed in logical concepts. A logical time model has been developed as a part of the official OMG UML profile MARTE, in order to enrich the formalism of this profile and also to facilitate the description and analysis of temporal constraints.
This time model is associated with CCSL (Clock Constraint Specification Language). Once the software is modeled, the difficulty lies in both expressing the relevant properties and in verifying them formally. We present an automatic transformation technique related to a method for verifying properties by model checking, thus exploiting both the CDL language (Context Description Language) and the OBP tool (Observer-based Prover). The technique is based on a translation of MARTE models and the CCSL constraints into Fiacre code. CDL can express predicates and observers. These are verified during the exhaustive exploration of the complete model by OBP. We illustrate our contribution by an illustrative case.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
André, C.: Syntax and semantics of the clock constraint specification language ccsl. Technical Report 6925, INRIA (2009)
André, C.: Verification of clock constraints: Ccsl observers in esterel. Technical Report 7211, INRIA (2010)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)
Dhaussy, P., Boniol, F., Roger, J.-C., Leroux, L.: Improving model checking with context modelling. In: Advances in Software Engineering, ID 547157, 13 pages (2012)
DeAntoni, J., Mallet, F., André, C.: Timesquare: on the formal execution of uml and dsl models. In: Tool Session of the 4th Model Driven Development for Distributed Real Time Systems (2008)
Farail, P., Gaufillet, P., Peres, F., Bodeveix, J.-P., Filali, M., Berthomieu, B., Rodrigo, S., Vernadat, F., Garavel, H., Lang, F.: FIACRE: an intermediate language for model verification in the TOPCASED environment. In: European Congress on Embedded Real-Time Software (ERTS), Toulouse. SEE (January 2008)
Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST 1993, Twente. Workshops in Computing, pp. 83–96. Springer Verlag (June 1993)
IEEE. IEEE standard for property specification language (psl). Technical Report 1850 (2005)
Mallet, F.: Automatic Generation of Observers from MARTE/CCSL. In: RSP 2012 - International Symposium on Rapid System Prototyping, Tampere, Finlande, pp. 86–92. IEEE (October 2012)
Mallet, F., André, C., De Simone, R.: Ccsl: Specifying clock constraints with uml/marte. ISSE 4, 309–314 (2008)
OMG. Uml profile for marte, v1.1. Object Managment Group, Document number: PTC/10-08-32 (August 2010)
Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
Yin, L., Mallet, F.: Correct transformation from ccsl to promela for verification. Technical Report 7491, INRIA (2011)
Yu, H., Talpin, J.-P., Besnard, L., Gautier, T., Marchand, H., Le Guernic, P.: Polychronous controller synthesis from marte ccsl timing specifications. In: Memocode (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Menad, N., Dhaussy, P. (2013). A Transformation Approach for Multiform Time Requirements. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds) Software Engineering and Formal Methods. SEFM 2013. Lecture Notes in Computer Science, vol 8137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40561-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-40561-7_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40560-0
Online ISBN: 978-3-642-40561-7
eBook Packages: Computer ScienceComputer Science (R0)