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
Erschienen in:
Buchtitelbild

2017 | OriginalPaper | Buchkapitel

From LOTOS to LNT

verfasst von : Hubert Garavel, Frédéric Lang, Wendelin Serwe

Erschienen in: ModelEd, TestEd, TrustEd

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We revisit the early publications of Ed Brinksma devoted, on the one hand, to the definition of the formal description technique LOTOS (ISO International Standard 8807:1989) for specifying communication protocols and distributed systems, and, on the other hand, to two proposals (Extended LOTOS and Modular LOTOS) for making LOTOS a simpler and more expressive language. We examine how this scientific agenda has been dealt with during the last decades. We review the successive enhancements of LOTOS that led to the definition of three languages: E-LOTOS (ISO International Standard 15437:2001), then LOTOS NT, and finally LNT. We present the software implementations (compilers and translators) developed for these new languages and report about their use in various application domains.

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
Nächstes Kapitel LOTOS-Like Composition of Boolean Nets and Causal Set Construction
Fußnoten
Literatur
1.
Abid, R., Salaün, G., Bongiovanni, F., De Palma, N.: Verification of a dynamic management protocol for cloud applications. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 178–192. Springer, Cham (2013). doi:10.​1007/​978-3-319-02444-8_​14 CrossRef
2.
3.
Arnold, F., Belinfante, A., Van der Berg, F., Guck, D., Stoelinga, M.: DFTCalc: a tool for efficient fault tree analysis. In: Bitsch, F., Guiochet, J., Kaâniche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 293–301. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-40793-2_​27 CrossRef
4.
Berthomieu, B., Bodeveix, J.P., Farail, P., Filali, M., Garavel, H., Gaufillet, P., Lang, F., Vernadat, F.: FIACRE: an intermediate language for model verification in the TOPCASED environment. In: Laprie, J.C. (ed.) Proceedings of the 4th European Congress on Embedded Real-Time Software (ERTS 2008), Toulouse, France, January 2008
5.
Berthomieu, B., Le Sergent, T.: Programming with behaviors in an ML framework — the syntax and semantics of LCS. In: Sannella, D. (ed.) ESOP 1994. LNCS, vol. 788, pp. 89–104. Springer, Heidelberg (1994). doi:10.​1007/​3-540-57880-3_​6 CrossRef
6.
Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. ISDN Syst. 14(1), 25–59 (1988)CrossRef
7.
Boullier, P., Jourdan, M.: A new error repair and recovery scheme for lexical and syntactic analysis. Sci. Comput. Program. 9(3), 271–286 (1987)CrossRef
8.
Boyer, F., Gruber, O., Salaün, G.: Specifying and verifying the SYNERGY reconfiguration protocol with LOTOS NT and CADP. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 103–117. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-21437-0_​10 CrossRef
9.
Brinksma, E., Leih, G.: Enhancements of LOTOS. In: Bolognesi, T., Lagemaat, J., Vissers, C. (eds.) LOTOSphere: Software Development with LOTOS, pp. 453–466. Kluwer Academic Publishers, Dordrecht (1995)CrossRef
10.
Brinksma, E.: A tutorial on LOTOS. In: Diaz, M. (ed.) Proceedings of the 5th IFIP International Workshop on Protocol Specification, Testing and Verification (PSTV 1885), Moissac, France, pp. 171–194. North-Holland, Amsterdam, June 1985
11.
Brinksma, E.: On the design of Extended LOTOS - a specification language for open distributed systems. Ph.D. thesis, University of Twente, November 1988
12.
Brinksma, E.: Constraint-oriented specification in a constructive formal description technique. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 130–152. Springer, Heidelberg (1990). doi:10.​1007/​3-540-52559-9_​63 CrossRef
13.
Brinksma, E.: Task 1.4 Deliverable on Language Enhancements, LOTOSphere (ESPRIT Projet 2304) Document ref. Lo/WP1/T1.4/N0016/V3, 146 p., April 1992
14.
Brinksma, E., Karjoth, G.: A specification of the OSI transport service in LOTOS. In: Yemini, Y., Strom, R.E., Yemini, S. (eds.) Proceedings of the 4th IFIP International Workshop on Protocol Specification, Testing and Verification, Skytop Lodge, PA, USA, pp. 227–251. North-Holland, Amsterdam, June 1984
15.
Brinksma, E., Katoen, J.P., Langerak, R., Latella, D.: A stochastic causality-based process algebra. Comput. J. 38(7), 552–565 (1995)CrossRef
16.
Brinksma, E., Tretmans, J., Verhaard, L.: A framework for test selection. In: Jonsson, B., Parrow, J., Pehrson, B. (eds.) Proceedings of the IFIP WG6.1 9th International Symposium on Protocol Specification, Testing and Verification, Stockholm, Sweden. pp. 233–248. North-Holland, Amsterdam, June 1991
17.
18.
CCITT: Specification and Description Language. Recommendation Z.100, International Consultative Committee for Telephony and Telegraphy, Geneva, March 1988
19.
Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., McKinty, C., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference Manual of the LNT to LOTOS Translator (Version 6.7), INRIA, Grenoble, France, July 2017
20.
Chebieb, A., Ameur, Y.A.: Formal verification of plastic user interfaces exploiting domain ontologies. In: Zhiqiu, H., Jun, S. (eds.) Proceedings of the International Symposium on Theoretical Aspects of Software Engineering (TASE 2015), Nanjing, China, pp. 79–86. IEEE Computer Society, Washington, D.C. (2015)
21.
Clark, R.G., Moreira, A.: Use of E-LOTOS in adding formality to UML. J. Univers. Comput. Sci. 6(11), 1071–1087 (2000)MATH
22.
Courtiat, J., Santos, C.A.S., Lohr, C., Outtaj, B.: Experience with RT-LOTOS, a temporal extension of the LOTOS formal description technique. Comput. Commun. 23(12), 1104–1123 (2000)CrossRef
23.
24.
de Souza, W.L., et al.: Design of distributed multimedia applications (DAMD). In: Hutter, D., Stephan, W., Traverso, P., Ullmann, M. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 77–91. Springer, Heidelberg (1999). doi:10.​1007/​3-540-48257-1_​4 CrossRef
25.
Ehrig, H., Fey, W., Hansen, H.: An algebraic specification language with two levels of semantics. Bericht No. 83-03, Fachbereich 20-Informatik, Technische Universität Berlin (1983)
26.
27.
Etchevers, X., Salaün, G., Boyer, F., Coupaye, T., Palma, N.D.: Reliable self-deployment of distributed cloud applications. Softw. Pract. Exp. 47(1), 3–20 (2017)CrossRef
28.
Evrard, H.: Génération automatique d’implémentation distribuée à partir de modèles formels de processus concurrents asynchrones. Thèse de Doctorat, Université de Grenoble, July 2015
29.
Evrard, H.: DLC: compiling a concurrent system formal specification to a distributed implementation. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 553–559. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49674-9_​34 CrossRef
30.
Evrard, H., Lang, F.: Formal verification of distributed branching multiway synchronization protocols. In: Beyer, D., Boreale, M. (eds.) FMOODS/FORTE -2013. LNCS, vol. 7892, pp. 146–160. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-38592-6_​11 CrossRef
31.
Evrard, H., Lang, F.: Automatic distributed code generation from formal models of asynchronous concurrent processes. In: Aldinucci, M., Daneshtalab, M., Leppänen, V., Lilius, J. (eds.) Proceedings of the 23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing - Special Session on Formal Approaches to Parallel and Distributed Systems (PDP/4PAD 2015), Turku, Finland, pp. 459–466. IEEE Computer Society Press, Washington, D.C., March 2015
32.
Evrard, H., Lang, F.: Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous. J. Log. Algebr. Methods Program. 88, 121–153 (2017)MathSciNetCrossRefMATH
33.
Garavel, H.: Utilisation du système CESAR pour la vérification de protocoles spécifiés en LOTOS. Rapport SPECTRE C2, Laboratoire de Génie Informatique - Institut IMAG, Grenoble, December 1986
34.
Garavel, H.: Vérification de programmes LOTOS à l’aide du système QUASAR. Master’s thesis, Institut National Polytechnique de Grenoble, September 1986
35.
Garavel, H.: Compilation of LOTOS abstract data types. In: Vuong, S.T. (ed.) Proceedings of the 2nd International Conference on Formal Description Techniques FORTE 1989, Vancouver BC, Canada, pp. 147–162. North-Holland, Amsterdam, December 1989
36.
Garavel, H.: On the introduction of gate typing in E-LOTOS. In: Dembinski, P., Sredniawa, M. (eds.) Proceedings of the 15th IFIP International Workshop on Protocol Specification, Testing and Verification (PSTV 1995), Warsaw, Poland, pp. 283–298. Chapman & Hall, New York, June 1995
37.
Garavel, H.: OPEN/CÆSAR: an open software architecture for verification, simulation, and testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68–84. Springer, Heidelberg (1998). doi:10.​1007/​BFb0054165 CrossRef
38.
Garavel, H.: Défense et illustration des algèbres de processus. In: Mammeri, Z. (ed.) Actes de l’Ecole d’été Temps Réel ETR 2003, Toulouse, France. Institut de Recherche en Informatique de Toulouse, September 2003
39.
Garavel, H.: Reflections on the future of concurrency theory in general and process calculi in particular. In: Palamidessi, C., Valencia, F.D. (eds.) Proceedings of the LIX Colloquium on Emerging Trends in Concurrency Theory, Ecole Polytechnique de Paris, France, 13–15 November 2006. Electronic Notes in Theoretical Computer Science, vol. 209, pp. 149–164. Elsevier Science Publishers, Amsterdam, April 2008. Also available as INRIA Research Report RR-6368
40.
41.
Garavel, H., Hermanns, H.: On combining functional verification and performance evaluation using CADP. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 410–429. Springer, Heidelberg (2002). doi:10.​1007/​3-540-45614-7_​23 CrossRef
42.
Garavel, H., Lang, F.: SVL: a scripting language for compositional verification. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) FORTE 2001. IIFIP, vol. 69, pp. 377–392. Kluwer Academic Publishers, Dordrecht (2002). doi:10.​1007/​0-306-47003-9_​24 CrossRef
43.
Garavel, H., Lang, F.: NTIF: a general symbolic model for communicating sequential processes with data. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 276–291. Springer, Heidelberg (2002). doi:10.​1007/​3-540-36135-9_​18 CrossRef
44.
45.
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. (STTT) 15(2), 89–107 (2013). SpringerCrossRefMATH
46.
Garavel, H., Salaün, G., Serwe, W.: On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP. Sci. Comput. Program. 74(3), 100–127 (2009)MathSciNetCrossRefMATH
47.
Garavel, H., Serwe, W.: The unheralded value of the multiway rendezvous: illustration with the production cell benchmark. In: Hermanns, H., Höfner, P. (eds.) Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), Uppsala, Sweden, vol. 244, pp. 230–270. Electronic Proceedings in Theoretical Computer Science, April 2017
48.
Garavel, H., Sifakis, J.: Compilation and verification of LOTOS specifications. In: Logrippo, L., Probert, R.L., Ural, H. (eds.) Proceedings of the 10th IFIP International Symposium on Protocol Specification, Testing and Verification (PSTV 1990), Ottawa, Canada, pp. 379–394. North-Holland, Amsterdam, June 1990
49.
Garavel, H., Sighireanu, M.: On the introduction of exceptions in LOTOS. In: Gotzhein, R., Bredereke, J. (eds.) Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE/PSTV 1996), Kaiserslautern, Germany, pp. 469–484. Chapman & Hall, New York, October 1996
50.
Garavel, H., Sighireanu, M.: Towards a second generation of formal description techniques - rationale for the design of E-LOTOS. In: Groote, J.F., Luttik, B., Wamel, J. (eds.) Proceedings of the 3rd International Workshop on Formal Methods for Industrial Critical Systems (FMICS 1998), Amsterdam, The Netherlands, pp. 187–230. CWI, Amsterdam, May 1998. Invited lecture
51.
Garavel, H., Sighireanu, M.: A graphical parallel composition operator for process algebras. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Formal Methods for Protocol Engineering and Distributed Systems. IAICT, vol. 28, pp. 185–202. Kluwer Academic Publishers, Dordrecht (1999)CrossRef
52.
Garavel, H., Thivolle, D.: Verification of GALS systems by combining synchronous languages and process calculi. In: Păsăreanu, C.S. (ed.) SPIN 2009. LNCS, vol. 5578, pp. 241–260. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-02652-2_​20 CrossRef
53.
Graf-Brill, A., Hermanns, H., Garavel, H.: A model-based certification framework for the EnergyBus standard. In: Ábrahám, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 84–99. Springer, Heidelberg (2014). doi:10.​1007/​978-3-662-43613-4_​6 CrossRef
54.
Guck, D., Spel, J., Stoelinga, M.: DFTCalc: reliability centered maintenance via fault tree analysis (tool paper). In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 304–311. Springer, Cham (2015). doi:10.​1007/​978-3-319-25423-4_​19 CrossRef
55.
Güdemann, M., Salaün, G., Ouederni, M.: Counterexample guided synthesis of monitors for realizability enforcement. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 238–253. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-33386-6_​20 CrossRef
56.
Huecas, G., Llana-Díaz, L., Quemada, J., Robles, T., Verdejo, A.: Process calculi: E-LOTOS. In: Bowman, H., Derrick, J. (eds.) Formal Methods for Distributed Processing: A Survey of Object-Oriented Approaches, pp. 77–104. Cambridge University Press, Cambridge (2001)
57.
Huecas, G., Llana-Díaz, L., Robles, T., Verdejo, A.: E-LOTOS: an overview. In: Marsan, M.A., Quemada, J., Robles, T., Silva, M. (eds.) Proceedings of the Workshop on Formal Methods and Telecommunications (WFMT’99), Zaragoza, Spain, pp. 94–102. Prensas Universitarias de Zaragoza, September 1999
58.
ISO/IEC: LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. Draft International Standard 8807, International Organization for Standardization - Information Processing Systems - Open Systems Interconnection, Geneva, July 1987
59.
ISO/IEC: ESTELLE - A Formal Description Technique Based on an Extended State Transition Model. International Standard 9074, International Organization for Standardization - Information Processing Systems - Open Systems Interconnection, Geneva, September 1988
60.
ISO/IEC: LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization - Information Processing Systems - Open Systems Interconnection, Geneva, September 1989
61.
ISO/IEC: Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization - Information Technology, Geneva, September 2001
62.
Jebali, F., Lang, F., Mateescu, R.: Formal modelling and verification of GALS systems using GRL and CADP. Formal Asp. Comput. 28(5), 767–804 (2016)MathSciNetCrossRefMATH
63.
Jourdan, M., Parigot, D.: Application development with the FNC-2 attribute grammar system. In: Hammer, D. (ed.) CC 1990. LNCS, vol. 477, pp. 11–25. Springer, Heidelberg (1991). doi:10.​1007/​3-540-53669-8_​71 CrossRef
64.
Kriouile, A., Serwe, W.: Formal analysis of the ACE specification for cache coherent systems-on-chip. In: Pecheur, C., Dierkes, M. (eds.) FMICS 2013. LNCS, vol. 8187, pp. 108–122. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-41010-9_​8 CrossRef
65.
Kriouile, A., Serwe, W.: Using a formal model to improve verification of a cache-coherent system-on-chip. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 708–722. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46681-0_​62
66.
67.
Lang, F.: Exp.Open 2.0: a flexible tool integrating partial order, compositional, and on-the-fly verification methods. In: Romijn, J., Smith, G., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 70–88. Springer, Heidelberg (2005). doi:10.​1007/​11589976_​6. Full version available as INRIA Research Report RR-5673CrossRef
68.
Lang, F., Salaün, G., Hérilier, R., Kramer, J., Magee, J.: Translating FSP into LOTOS and networks of automata. Formal Asp. Comput. 22(6), 681–711 (2010)CrossRefMATH
69.
Lantreibecq, E., Serwe, W.: Formal analysis of a hardware dynamic task dispatcher with CADP. Sci. Comput. Program. 80(Part A), 130–149 (2014)CrossRef
70.
Leduc, G., Jeffrey, A., Sighireanu, M.: Introduction à E-LOTOS. In: Cavalli, A. (ed.) Ingénierie des protocoles et qualité de service. Collection IC2, chap. 6, pp. 213–253. Hermès, Paris (2001)
71.
Léonard, L., Leduc, G.: An introduction to ET-LOTOS for the description of time-sensitive systems. Comput. Netw. ISDN Syst. 29(3), 271–292 (1997)CrossRef
72.
Léonard, L., Leduc, G.: A formal definition of time in LOTOS. Formal Asp. Comput. 10(3), 248–266 (1998)CrossRefMATH
73.
Li, X., Madnick, S., Zhu, H., Fan, Y.: Improving data quality for web services composition. In: Proceedings of the 7th International Workshop on Quality in Databases (QDB 2009), Lyon, France, August 2009
74.
Massetto, F.I., de Souza, W.L., Zorzo, S.D.: Simulator for E-LOTOS specifications. In: Proceedings of the 35th Annual Simulation Symposium (SS 2002), San Diego, California, USA, pp. 389–394. IEEE Computer Society, Washington, D.C., April 2002
75.
Mateescu, R.: A generic framework for model checking software architectures. In: Augusto, J.C., Ultes-Nitsche, U. (eds.) Proceedings of the 2nd International Workshop on Verification and Validation of Enterprise Information Systems (VVEIS 2004), Porto, Portugal. INSTICC Press, April 2004. Keynote presentation
76.
Mateescu, R., Monteiro, P.T., Dumas, E., de Jong, H.: Computation tree regular logic for genetic regulatory networks. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 48–63. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-88387-6_​6 CrossRef
77.
Mateescu, R., Salaün, G.: PIC2LNT: model transformation for model checking an applied pi-calculus. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 192–198. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-36742-7_​14 CrossRef
78.
Mateescu, R., Serwe, W.: Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols. Sci. Comput. Program. 78(7), 843–861 (2013)CrossRef
79.
Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-68237-0_​12 CrossRef
80.
de Meer, J., Roth, R., Vuong, S.: Introduction to algebraic specifications based on the language ACT ONE. Comput. Netw. ISDN Syst. 23(5), 363–392 (1992)CrossRef
81.
Milne, G.J.: CIRCAL and the representation of communication, concurrency, and time. ACM Trans. Progr. Lang. Syst. 7(2), 270–298 (1985)CrossRefMATH
82.
83.
84.
Mkaouar, H., Zalila, B., Hugues, J., Jmaiel, M.: From AADL model to LNT specification. In: de la Puente, J.A., Vardanega, T. (eds.) Ada-Europe 2015. LNCS, vol. 9111, pp. 146–161. Springer, Cham (2015). doi:10.​1007/​978-3-319-19584-1_​10 CrossRef
85.
Oliveira, R., Dupuy-Chessa, S., Calvary, G., Dadolle, D.: Using formal models to cross check an implementation. In: Luyten, K., Palanque, P. (eds.) Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2016), Brussels, Belgium, pp. 126–137. ACM, New York, June 2016
86.
Poizat, P., Salaün, G.: Checking the realizability of BPMN 2.0 choreographies. In: Proceedings of the 27th Symposium On Applied Computing (SAC 2012), Riva del Garda, Italy. ACM Press, New York, March 2012
87.
88.
Ponsini, O., Fédèle, C., Kounalis, E.: Rewriting of imperative programs into logical equations. Sci. Comput. Program. 56(3), 363–401 (2005)MathSciNetCrossRefMATH
89.
90.
Roth, R., de Meer, J., Storp, S.: Data specifications in Modular LOTOS. In: Bolognesi, T., Lagemaat, J., Vissers, C. (eds.) LOTOSphere: Software Development with LOTOS, pp. 467–479. Kluwer Academic Publishers, Dordrecht (1995)CrossRef
91.
Serwe, W.: Formal specification and verification of fully asynchronous implementations of the Data Encryption Standard. In: van Glabbeek, R., Groote, J.F., Höfner, P. (eds.) Proceedings of the International Workshop on Models for Formal Analysis of Real Systems (MARS 2015), Suva, Fiji. Electronic Proceedings in Theoretical Computer Science, vol. 196. Open Publishing Association (2015)
92.
Shankland, C., Verdejo, A.: Time, E-LOTOS, and the FireWire. In: Marsan, M.A., Quemada, J., Robles, T., Silva, M. (eds.) Proceedings of the Workshop on Formal Methods and Telecommunications (WFMT 1999), Zaragoza, Spain, pp. 103–119. Prensas Universitarias de Zaragoza, September 1999
93.
Shankland, C., Verdejo, A.: A case study in abstraction using E-LOTOS and the FireWire. Comput. Netw. 37(3/4), 481–502 (2001)CrossRef
94.
Sighireanu, M.: Contribution à la définition et à l’implémentation du langage “Extended LOTOS”. Thèse de Doctorat, Université Joseph Fourier (Grenoble), January 1999
95.
96.
Sighireanu, M., Turner, K.: Requirement capture, formal description and verification of an invoicing system. Research Report RR-3575, INRIA, Grenoble, December 1998
97.
Stöcker, J., Lang, F., Garavel, H.: Parallel processes with real-time and data: the ATLANTIF intermediate format. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 88–102. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-00255-7_​7 CrossRef
98.
Thivolle, D.: Langages modernes pour la vérification des systèmes asynchrones. Thèse de Doctorat, Université Joseph Fourier, Grenoble, France and Universitatea Politehnica din Bucuresti, Bucharest, Romania, April 2011
99.
Turner, K.J., Sighireanu, M.: (E)-Lotos: (enhanced) language of temporal ordering specification. In: Frappier, M., Habrias, H. (eds.) Software Specification Methods: An Overview Using a Case Study, pp. 166–190. Springer, London (2001). doi:10.​1007/​978-1-4471-0701-9_​10
100.
Vekris, D., Lang, F., Dima, C., Mateescu, R.: Verification of EB3 specifications using CADP. Formal Asp. Comput. 28(1), 145–178 (2016)MathSciNetCrossRefMATH
101.
Verdejo, A.: E-LOTOS: Tutorial and Semantics. Master’s thesis, Departamento de Sistemas Informáticos y Programación, Universidad Complutense de Madrid, Spain, June 1999
102.
Wu, H., Yang, X., Katoen, J.-P.: Performance evaluation of concurrent data structures. In: Fränzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 38–49. Springer, Cham (2016). doi:10.​1007/​978-3-319-47677-3_​3 CrossRef
103.
Zhang, Z., Serwe, W., Wu, J., Zheng, T.Y.H., Myers, C.: An improved fault-tolerant routing algorithm for a network-on-chip derived with formal analysis. Sci. Comput. Program. 118, 24–39 (2016)CrossRef
Metadaten
Titel
From LOTOS to LNT
verfasst von
Hubert Garavel
Frédéric Lang
Wendelin Serwe
Copyright-Jahr
2017
Buch
ModelEd, TestEd, TrustEd

Print ISBN: 978-3-319-68269-3

Electronic ISBN: 978-3-319-68270-9

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-68270-9_1

Premium Partner

    Bildnachweise