Abstract
The UML Profile for Modeling and Analysis of Real-Time and Embedded systems promises a general modeling framework to design and analyze systems. Lots of works have been published on the modeling capabilities offered by MARTE, much less on verification techniques supported. The Clock Constraint Specification Language (CCSL), first introduced as a companion language for MARTE, was devised to offer a formal support to conduct causal and temporal analyses on MARTE models.
This work introduces formally a state-based semantics for CCSL operators and then focuses on the analysis capabilities of MARTE/CCSL and more particularly on boundness issues.
The approach is illustrated on one simple example where the architecture plays an important role. We describe a process where the logical description of the application is progressively refined to take into account the candidate execution platforms through allocation.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
OMG: UML Profile for MARTE, v1.0. Object Management Group. (November 2009) formal/2009-11-02
André, C., Mallet, F., de Simone, R.: Modeling time(s). In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 559–573. Springer, Heidelberg (2007)
André, C.: Syntax and semantics of the Clock Constraint Specification Language (CCSL). Research Report 6925, INRIA (May 2009)
DeAntoni, J., Mallet, F.: Timesquare: Treat your models with logical time. In: Furia, C.A., Nanz, S. (eds.) TOOLS 2012. LNCS, vol. 7304, pp. 34–41. Springer, Heidelberg (2012)
Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Le Guernic, P., de Simone, R.: The synchronous languages 12 years later. Proc. of the IEEE 91(1), 64–83 (2003)
Le Guernic, P., Talpin, J.P., Le Lann, J.C.: Polychrony for system design. Journal of Circuits, Systems, and Computers 12(3), 261–304 (2003)
Lee, E.A., Sangiovanni-Vincentelli, A.L.: A framework for comparing models of computation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 17(12), 1217–1229 (1998)
Arnold, A.: Finite transition systems - semantics of communicating systems. Int. Series in Computer Science. Prentice Hall (1994)
Kahn, G.: The semantics of simple language for parallel programming. In: IFIP Congress, pp. 471–475 (1974)
Buck, J.T.: Scheduling Dynamic Dataflow Graphs with Bounded Memory Using the Token Flow Model. PhD thesis, U.C. Berkeley (1993)
Commoner, F., Holt, A.W., Even, S., Pnueli, A.: Marked directed graphs. J. Comput. Syst. Sci. 5(5), 511–523 (1971)
Lee, E., Messerschmitt, D.: Synchronous data flow. Proceedings of the IEEE 75(9), 1235–1245 (1987)
Feiler, P.H., Hansson, J.: Flow latency analysis with the architecture analysis and design language. Technical Report CMU/SEI-2007-TN-010, CMU (June 2007)
Society of Automotive Engineers, SAE Architecture Analysis and Design Language (AADL) (June 2006) document number: AS5506/1
Yin, L., Mallet, F., Liu, J.: Verification of MARTE/CCSL time requirements in Promela/SPIN. In: ICECCS, pp. 65–74. IEEE Computer Society (2011)
Gascon, R., Mallet, F., DeAntoni, J.: Logical time and temporal logics: Comparing UML MARTE/CCSL and PSL. In: Combi, C., Leucker, M., Wolter, F. (eds.) TIME, pp. 141–148. IEEE (2011)
Romenska, Y., Mallet, F.: Lazy parallel synchronous composition of infinite transition systems. In: ICTERI. CEUR Workshop Proc., vol. 1000, pp. 130–145 (2013)
Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Times: A tool for schedulability analysis and code generation of real-time systems. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 60–72. Springer, Heidelberg (2004)
Krčál, P., Yi, W.: Decidable and undecidable problems in schedulability analysis using timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 236–250. Springer, Heidelberg (2004)
Abdeddaim, Y., Asarin, E., Maler, O.: Scheduling with timed automata. Theoretical Computer Science 354(2), 272–300 (2006)
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Alur, R., Weiss, G.: Regular specifications of resource requirements for embedded control software. In: IEEE Real-Time and Embedded Technology and Applications Symp., pp. 159–168. IEEE CS (2008)
Alur, R., Weiss, G.: Rtcomposer:a framework for real-time components with scheduling interfaces. In: Int. Conf. on Embedded Software, EMSOFT 2008, pp. 159–168. ACM (2008)
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
Mallet, F., Millo, JV. (2013). Boundness Issues in CCSL Specifications. In: Groves, L., Sun, J. (eds) Formal Methods and Software Engineering. ICFEM 2013. Lecture Notes in Computer Science, vol 8144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41202-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-41202-8_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41201-1
Online ISBN: 978-3-642-41202-8
eBook Packages: Computer ScienceComputer Science (R0)