nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Linear Temporal Logic Applied to Component-Based Software Architectural Models Specified Through \(\rho _{\mathrm {arq}}\) Calculus

verfasst von : Oscar Javier Puentes, Henry Alberto Diosa

Erschienen in: Applied Computer Sciences in Engineering

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

This paper reports a mechanism to incorporate Linear Temporal Logic (LTL) for a component-based software architectural configuration specified by the \(\rho _{arq}\)-calculus. This process was made through the translation of the system definition, structure and behavior, to Atomic Propositions Transition System (APTS), upon which, the verification of one property was performed using LTL. The PintArq software application was extended to support this mechanism. One example ilustrates the verification of responsiveness, a subtype of liveness property.

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

Vorheriges Kapitel Modelling Collaborative Logistics Policies that Impact the Performance of the Agricultural Sector

Nächstes Kapitel Design of App Based on Hl7 and IoT for Assistance PHD Health Programs

Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181–185 (1985)MathSciNetCrossRef

Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)CrossRef

Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, London (2008)MATH

Barendregt, H., Barendsen, E.: Introduction to lambda calculus. Nieuw archief voor wisenkunde 4(Mar), 337–372 (2000). http://homepages.nyu.edu/~cb125/Lambda/barendregt.94.pdf

Biswas, S., Deka, J.K.: NPTEL: Computer Science and Engineering - Design Verification and Test of Digital VLSI Circuits (2014). http://nptel.ac.in/courses/106103116/19

Cheung, S.C., Giannakopoulou, D., Kramer, J.: Verification of liveness properties using compositional reachability analysis. In: Jazayeri, M., Schauer, H. (eds.) ESEC/SIGSOFT FSE -1997. LNCS, vol. 1301, pp. 227–243. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63531-9_17CrossRef

Cirstea, H., Kirchner, C.: \(\rho \)-Calculus. Its Syntax and Basic Properties, vol. 53, no. 9 (1998)

Clarke, E.: Model Checking. MIT Press, London (2000)

Diosa, H., Díaz Frías, J.F., Gaona, C.M.: Especificación formal de arquitecturas de software basadas en componentes: chequeo de corrección con cálculo rho-arq, no. 12 (2010)

10.

Diosa, H.A., Díaz, J.F., Gaona C.M.: Cálculo para el modelado formal de arquitecturas de software basadas en componentes: cálculo \(\rho _{arq}\). Revista Científica. Universidad Distrital Francisco José de Caldas, no. 12 (2010)

11.

Bertolino, A., Inverardi, P., Muccini, H.: Formal methods in testing software architectures. In: Bernardo, M., Inverardi, P. (eds.) SFM 2003. LNCS, vol. 2804, pp. 122–147. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-39800-4_7CrossRef

12.

Micskei, Z., Waeselynck, H.: The many meanings of UML 2 sequence diagrams: a survey. Softw. Syst. Model. 10(4), 489–514 (2010). https://doi.org/10.1007/s10270-010-0157-9CrossRef

13.

Milner, R.: Communicating and Mobile Systems: The Pi Calculus. Cambridge University Press, Cambridge (1999)MATH

14.

Montoya Serna, E.: Métodos formales e Ingeniería de Software. Revista Virtual Universidad Católica del Norte, no. 30, 1–26 (2011). http://revistavirtual.ucn.edu.co/index.php/RevistaUCN/article/view/62

15.

Niehren, J., Müller, M.: Constraints for free in concurrent computation. In: Kanchanasut, K., Lévy, J.-J. (eds.) ACSC 1995. LNCS, vol. 1023, pp. 171–186. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60688-2_43CrossRef

16.

Object Management Group: OMG Unified Modeling Language (OMG UML), version 2.5, March 2015

17.

Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4(3), 455–495 (1982)CrossRef

18.

Parrow, J.: An Introduction to the pi-Calculus (2001). http://homepages.nyu.edu/~cb125/Lambda/barendregt.94.pdf

19.

Rico, J.A.: Representación visual de la ejecución de una arquitectura de software basada en componentes con especificación formal en cálculo \(\rho \)arq (2015)

20.

Smolka, G.: A calculus for higher-order concurrent constraint programming with deep guards. Technical report, Bundesminister für Forschung und Technologie (1994)

21.

Smolka, G.: A Foundation for Higher-order Concurrent Constraint Programming. Tech. rep., Bundesminister für Forschung und Technologie (1994)

22.

Wing, J.M.: FAQ on \(\pi \)-Calculus, pp. 1–8, December 2002

Titel: Linear Temporal Logic Applied to Component-Based Software Architectural Models Specified Through Calculus
verfasst von: Oscar Javier Puentes
Henry Alberto Diosa
Verlag: Springer International Publishing
Buch: Applied Computer Sciences in Engineering
Print ISBN: 978-3-030-00349-4

Electronic ISBN: 978-3-030-00350-0

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-030-00350-0_33

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"