Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 1/2015

01.02.2015 | Regular Paper

Real-time specifications

verfasst von: Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, Louis-Marie Traonouez, Andrzej Wąsowski

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 1/2015

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation, and a set of operators supporting stepwise design. We develop a specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications—all indispensable ingredients of a compositional design methodology. The theory is implemented in the new tool Ecdar. We present symbolic versions of the algorithms used in Ecdar, and demonstrate the use of the tool using a small case study in compositional verification.
Vorheriger Artikel Assessing the effects of introducing a new software development process: a methodological description
Nächster Artikel Termination proofs for linear simple loops

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Fußnoten
1
The quotient generates components that cannot be displayed in the GUI.
 
2
Ecdar borrows from Uppaal the syntactic constructs to obtain this effect conveniently: urgent locations and urgent channels.
 
Literatur
1.
Abdellatif, T., Combaz, J., Sifakis, J.: Model-based implementation of real-time applications. In: EMSOFT, pp. 229–238. ACM, New York (2010)
2.
Adler, B.T, de Alfaro, L., Dias, L., de Silva, F.M., Legay, A., Raman, V., Ticc, P.R.: A tool for interface compatibility and composition. In: CAV, vol. 4144 of LNCS, pp. 59–62. Springer, Berlin (2006)
3.
4.
Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: CONCUR, vol. 1466 of LNCS. Springer, Berlin (1998)
5.
Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Times, W.Y.: A tool for schedulability analysis and code generation of real-time systems. In: FORMATS, vol. 2791 of LNCS, pp. 60–72. Springer, Berlin (2003)
6.
Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowsk, A.: Modal and mixed specifications: key decision problems and their complexities. Math Struct Comput Sci 20(1), 75–103 (2010)CrossRefMATH
7.
Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)
8.
Bauer, S.S., Juhl, L., Larsen, K.G., Legay, A., Srba, J.: Extending modal transition systems with structured labels. Math Struct Comput Sci 22(4), 581–617 (2012)CrossRefMATHMathSciNet
9.
Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: Uppaal-tiga: time for playing games! In: CAV, vol. 4590 of LNCS. Springer, Berlin (2007)
10.
Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing uppaal over 15 years. Softw. Pract. Exper. 41(2), 133–142 (2011)
11.
Berendsen, J., Vaandrager, F.W.: Compositional abstraction in real-time model checking. In: FORMATS, vol. 5215 of LNCS. Springer, Berlin (2008)
12.
Bertrand, N., Legay, A., Pinchinat, S., Raclet, J.-B.: A compositional approach on modal specifications for timed systems. In ICFEM, LNCS. Springer, Berlin (2009)
13.
Bourke, T., Sowmya, A.: Automatically transforming and relating uppaal models of embedded systems. In EMSOFT, pp. 59–68. ACM, New York (2008)
14.
Bourke, T., David, A., Larsen, K.G., Legay, A., Lime, D., Nyman, U., Wasowski, A.: New results on timed specifications. In: WADT, vol. 7137 of LNCS, pp. 175–192. Springer, Berlin (2010)
15.
Bulychev, P., Chatain, T., David, A., Larsen, K.G.: Efficient on-the-fly algorithm for checking alternating timed simulation. In: FORMATS, vol. 5813 of LNCS, pp. 73–87. Springer, Berlin (2009)
16.
Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wąsowski, A.: Compositional design methodology with constraint Markov chains. In: QEST, pp. 123–132. IEEE Press, USA (2010)
17.
Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games, In: CONCUR (2005)
18.
Cassez, F., David, A., Larsen, K.G., Lime, D., Raskin, J.-F.: Timed control with observation based and stuttering invariant strategies. In: ATVA, vol. 4762 of LNCS, pp. 192–206. Springer, Berlin (2007)
19.
Cerans, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification—theory and tools. In: CAV, pp. 253–267. Springer, Berlin (1993)
20.
Chakabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.I.A.: Resource interfaces. In: Alur. R., Lee, I., (eds) EMSOFT 03: 3rd International Workshop on Embedded Software, LNCS. Springer, Berlin (2003)
21.
Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Mang, F.Y.C.: Synchronous and bidirectional component interfaces. In: CAV, vol. 2404 of LNCS, pp. 414–427 (2002)
22.
Clarke, E.M., Orna, G.: Model Checking. The MIT Press, Cambridge (1999)
23.
David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Methodologies for specification of real-time systems using timed i/o automata. In: FMCO, vol. 6286 of LNCS, pp. 290–310. Springer, Berlin (2009)
24.
David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed i/o automata: a complete specification theory for real-time systems. In: HSCC, pp. 91–100. ACM, USA (2010)
25.
David, A., Larsen, K.G., Legay, A., Møller, M.H., Nyman, U., Ravn, A.P., Skou, A., Wasowski, A.: Compositional verification of real-time systems using ecdar. STTT 14(6), 703–720 (2012)
26.
David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Ecdar: An environment for compositional design and analysis of real time systems. In: ATVA, vol. 6252 of LNCS, pp. 365–370. Springer, Berlin (2010)
27.
de Alfaro, L.: Game models for open systems. In: Proceedings of the International Symposium on Verification (Theory in Practice), vol. 2772 of LNCS. Springer, Berlin (2003)
28.
de Alfaro, L., da Silva, L.D., Faella, M., Legay, A., Roy, P., Sorea, Ma.: Sociable interfaces. In: FroCos, vol. 3717 of LNCS, pp. 81–105. Springer, Berlin (2005)
29.
de Alfaro, L., Faella, M.: An accelerated algorithm for 3-color parity games with an application to timed games. In: CAV, vol. 4590 of LNCS. Springer, Berlin (2007)
30.
de Alfaro, L, Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: CONCUR, vol. 2761 of LNCS, pp. 142–156. Springer, Berlin (2003)
31.
de Alfaro, L., Henzinger, T.A.: Interface automata. In: FSE, pp. 109–120, Austria, September 2001. ACM Press, New York (2001)
32.
de Alfaro, L., Henzinger, T.A.: Interfacebased design. In: In Engineering Theories of Software Intensive Systems, Marktoberdorf Summer School. Kluwer Academic Publishers, Dordrecht (2004)
33.
de Alfaro, L., Henzinger, T.A., Majumdar, R.: Symbolic algorithms for infinite-state games. In: CONCUR, vol 2154 of LNCS, pp. 536–550. Springer, Berlin (2001)
34.
de Alfaro, L., Henzinger, T.A., Stoelinga, M.I.A.: Timed interfaces. In: EMSOFT, vol. 2491 of LNCS, pp. 108–122. Springer, Berlin (2002)
35.
Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wasowski, A.: Abstract probabilistic automata. In: VMCAI, pp. 324–339. Springer, Berlin (2011)
36.
Fiadeiro, J., Andrade, L.F.: Interconnecting objects via contracts. In: Proceedings of the 38th International Conference on Technology of Object-Oriented Languages and Systems, Components for Mobile Computing (TOOLS’38), pp. 182–183. IEEE Computer Society, USA (2001)
37.
Fiadeiro, J.L., Maibaum, T.S.E.: Interconnecting formalisms: Supporting modularity, reuse and incrementality. In: Proceedings of the 3rd ACM SIGSOFT Symposium on Foundations of Software Engineering (SIGSOFT FSE’95), pp. 72–80. ACM, New York (1995)
38.
Garland, S.J., Lynch, N.A.: The IOA Language and Toolset: Support for Designing, Analyzing, and Building Distributed Systems. Technical report. Massachusetts Institute of Technology, Cambridge (1998)
39.
Henzinger, T.A., Manna, Z., Pnueli, A.: Timed transition systems. In: REX Workshop, vol. 600 of LNCS, pp. 226–251. Springer, Berlin (1991)
40.
Henzinger, T.A., Matic, S.: An interface algebra for real-time components. In: IEEE Real Time Technology and Applications Symposium, pp. 253–266. IEEE Computer Society, USA (2006)
41.
Henzinger, T.A., Sifakis, J.: The embedded systems design challenge. In: FM, vol. 4085 of LNCS, pp. 1–15. Springer, Berlin (2006)
42.
Kaynar, D.K., Lynch, N.A., Segala, R., Vaandrager, F.W.: The Theory of Timed I/O Automata, 2nd edn. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael (2010)
43.
Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. In: FORMATS, vol. 3253 of LNCS, pp. 293–308. Springer, Berlin (2004)
44.
Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027–1077 (2007)CrossRefMATHMathSciNet
45.
Larsen, K.G.: Modal specifications. In: Sifakis, J., (ed) Automatic Verification Methods for Finite State Systems, vol. 407 of LNCS, pp. 232–246. Springer, Berlin (1989)
46.
Larsen, K.G., Legay, A., Traonouez, L.-M., Wasowski, A.: Robust specification of real time components. In: FORMATS 2011, vol. 6919 of LNCS. Springer, Berlin (2011)
47.
Larsen, K.G., Nyman, U., Wasowski, A.: Modal I/O automata for interface and product line theories. In: De Nicola, R., (ed) ESOP, vol. 4421 of LNCS, pp. 64–79. Springer, Berlin (2007)
48.
Larsen, Kim G., Pettersson, Paul, Yi, Wang: Model-Checking for Real-Time Systems. In Proc. of Fundamentals of Computation Theory, volume 965 of LNCS, pages 62–88, August (1995)
49.
Lynch, N.: I/O automata: a model for discrete event systems. In: Annual Conference on Information Sciences and Systems, pp. 29–38. Princeton University, Princeton (1988)
50.
Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. Technical Report MIT/LCS/TM-373. The MIT Press, Cambridge (1988)
51.
Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems (an extended abstract). In: STACS, pp. 229–242 (1995)
52.
Robin, M.: Communication and Concurrency. Prentice Hall, New York (1988)
53.
De Nicola, R., Segala, R.: A process algebraic view of input/output automata. Theor. Comput. Sci. 138(2), 391–423 (1995)
54.
Post, A., Hoenicke, J., Podelski, A.: rt-inconsistency: a new property for real-time requirements. In: FASE, vol. 6603 of LNCS, pp. 34–49. Springer, Berlin (2011)
55.
56.
Stark, E.W., Cleavland, R., Smolka, S.A.: A process-algebraic language for probabilistic I/O automata. In: CONCUR, LNCS, pp. 189–2003. Springer, Berlin (2003)
57.
Sun, J., Liu, Y., Dong, J.S.: Model checking csp revisited: Introducing a process analysis toolkit. In: ISoLA, vol. 17 of Communications in Computer and Information Science, pp. 307–322. Springer, Berlin (2008)
58.
Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., Étienne, A.: Modeling and verifying hierarchical real-time systems using stateful timed csp. ACM Trans. Softw. Eng. Methodol. 22(1), 3.1–3.29 (2013)
59.
60.
Traonouez, L.-M.: A parametric counterexample refinement approach for robust timed specifications. In: FIT, vol. 87 of EPTCS, pp. 17–33 (2012)
61.
Vaandrager, F.W.: On the relationship between process algebra and input/output automata. In: LICS, pp. 387–398 (1991)
62.
Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robust safety of timed automata. Formal Methods Syst. Design 33, 45–84 (2008)
63.
Yi, W.: Real-time behaviour of asynchronous agents. In: Baeten, J.C.M., Klop, J.W., (eds) CONCUR, vol. 458 of LNCS, pp. 502–520. Springer, Berlin (1990)
Metadaten
Titel
Real-time specifications
verfasst von
Alexandre David
Kim G. Larsen
Axel Legay
Ulrik Nyman
Louis-Marie Traonouez
Andrzej Wąsowski
Publikationsdatum
01.02.2015
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 1/2015
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-013-0286-x

Weitere Artikel der Ausgabe 1/2015

International Journal on Software Tools for Technology Transfer 1/2015 Zur Ausgabe

Regular Paper

Termination proofs for linear simple loops

Regular Paper

Assessing the effects of introducing a new software development process: a methodological description

Regular Paper

Functional prototypes for generic C++ libraries: a transformational approach based on higher-order, typed signatures

Regular Paper

Testing abstract behavioral specifications

Regular Paper

A construction and minimization service for continuous probability distributions

regular paper

A systematic review of state-based test tools

Premium Partner

    Bildnachweise