Abstract
It is critical to analyze characteristics of real-time embedded systems, such as timing behavior, early in the development. In the automotive domain, EAST-ADL is a concrete example of the model-based approach for the architectural modeling of real-time systems. The Timing Augmented Description Language v2 (TADL2) allows for the specification of timing constraints on top of EAST-ADL models. In this paper we propose a formal validation & verification methodology for timing behaviors given with TADL2. The formal semantics of the timing constraints is given as a mapping to the Clock Constraint Specification Language (CCSL), a formal language that implements the MARTE Time Model. Based on such a mapping, the validation is carried out by the simulation of TADL2 specifications. The simulation allows for a rapid prototyping of TADL2 specifications. The verification is performed based on a TADL2 mapping to timed automata modeling using the Uppaal model-checker. The whole process is illustrated on a Brake-By-Wire application.
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
BBW Spec in TADL2, http://www-sop.inria.fr/members/Arda.Goknil/bbw/
ITEA TIMMO-2-USE Project, http://timmo-2-use.org/
TADL2-CCSL QVTo Transformation, http://www-sop.inria.fr/members/Arda.Goknil/bbw/
Aegedal, J.: Quality of service support in development of distributed systems. PhD Thesis (2001)
Alfonso, A., Braberman, V.A., Kicillof, N., Olivero, A.: Visual timed event scenarios. In: ICSE 2004, pp. 168–177 (2004)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
André, C.: Syntax and semantics of the Clock Constraint Specification Language (CCSL). Research Report 6925, INRIA (May 2009)
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)
ATESST (Advancing Traffic Efficiency through Software Technology). East-ADL2 specification (March 20, 2008), http://www.atesst.org
Autosar Consortium. AUTOSAR specification, release 4.0 (2009), http://www.autosar.org/
DeAntoni, J., Mallet, F.: Timesquare: Treat your models with logical time. In: Furia, C.A., Nanz, S. (eds.) TOOLS Europe 2012. LNCS, vol. 7304, pp. 34–41. Springer, Heidelberg (2012)
Dvorak, R.: Model transformation with operational qvt. In: EclipseCon 2008 (2008)
Enoiu, E.P., Marinescu, R., Seceleanu, C.C., Pettersson, P.: Vital: A verification tool for EAST-ADL models using uppaal port. In: ICECCS 2012, pp. 328–337 (2012)
IEEE Standards Association. IEEE Standard for Verilog Hardware Description Language. Design Automation Standards Committee, IEEE Std 1364TM-2005 (2005)
Kang, E.-Y., Schobbens, P.-Y., Pettersson, P.: Verifying functional behaviors of automotive products in EAST-ADL2 using uppaal-port. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol. 6894, pp. 243–256. Springer, Heidelberg (2011)
Klein, F., Giese, H.: Joint structural and temporal property specification using timed story scenario diagrams. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol. 4422, pp. 185–199. Springer, Heidelberg (2007)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer 1(1-2), 134–152 (1997)
OMG. UML Profile for MARTE, v1.0. Object Management Group (November 2009) (formal/2009-11-02)
Peraldi-Frati, M.A., Goknil, A., DeAntoni, J., Nordlander, J.: A timing model for specifying multi clock automotive systems: The timing augmented description language v2. In: ICECCS 2012, pp. 230–239 (2012)
Qureshi, T.N., Chen, D.-J., Törngren, M.: A timed automata-based method to analyze EAST-ADL timing constraint specifications. In: Vallecillo, A., Tolvanen, J.-P., Kindler, E., Störrle, H., Kolovos, D. (eds.) ECMFA 2012. LNCS, vol. 7349, pp. 303–318. Springer, Heidelberg (2012)
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
Goknil, A., Suryadevara, J., Peraldi-Frati, MA., Mallet, F. (2013). Analysis Support for TADL2 Timing Constraints on EAST-ADL Models. In: Drira, K. (eds) Software Architecture. ECSA 2013. Lecture Notes in Computer Science, vol 7957. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39031-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-39031-9_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39030-2
Online ISBN: 978-3-642-39031-9
eBook Packages: Computer ScienceComputer Science (R0)