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
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
An Exercise in Mathematical Engineering: Stating and Proving Kuratowski Theorem Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

CSP and Kripke Structures

verfasst von : Ana Cavalcanti, Wen-ling Huang, Jan Peleska, Jim Woodcock

Erschienen in: Theoretical Aspects of Computing - ICTAC 2015

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

A runtime verification technique has been developed for CSP via translation of CSP models to Kripke structures. With this technique, we can check that a system under test satisfies properties of traces and refusals of its CSP model. This complements analysis facilities available for CSP and for all languages with a CSP-based semantics: Safety-Critical Java, Simulink, SysML, and so on. Soundness of the verification depends on the soundness of the translation and on the traceability of the Kripke structure analysis back to the CSP models and to the property specifications. Here, we present a formalisation of soundness by unifying the semantics of the languages involved: normalised graphs used in CSP model checking, action systems, and Kripke structures. Our contributions are the unified semantic framework and the formal argument itself.

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 Verifying Android’s Permission Model
Nächstes Kapitel Specifying and Analyzing the Kademlia Protocol in Maude
Literatur
1.
Anderson, H., Ciobanu, G., Freitas, L.: UTP and temporal logic model checking. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 22–41. Springer, Heidelberg (2010) CrossRef
2.
Back, R.J., Kurki-Suonio, R.: Distributed cooperation with action systems. ACM Trans. Program. Lang. Syst. 10(4), 513–554 (1988)CrossRefMATH
3.
Burdy, L., et al.: An overview of JML tools and applications. STTT 7(3), 212–232 (2005)CrossRef
4.
Butterfield, A.: A denotational semantics for Handel-C. FACJ 23(2), 153–170 (2011)MATH
5.
Cavalcanti, A.L.C., Clayton, P., O’Halloran, C.: From control law diagrams to Ada via \({\sf Circus}\). FACJ 23(4), 465–512 (2011)MATH
6.
7.
Cavalcanti, A., Woodcock, J.: A tutorial introduction to CSP in unifying theories of programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220–268. Springer, Heidelberg (2006) CrossRef
8.
Cavalcanti, A.L.C., Zeyda, F., Wellings, A., Woodcock, J.C.P., Wei, K.: Safety-critical Java programs from \({\sf Circus}\) models. RTS 49(5), 614–667 (2013)
9.
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014) CrossRef
10.
Haddad, G., Hussain, F., Leavens, G.T.: The design of SafeJML, a specification language for SCJ with support for WCET specification. In: JTRES. ACM (2010)
11.
Harwood, W.T., Cavalcanti, A., Woodcock, J.: A theory of pointers for the UTP. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 141–155. Springer, Heidelberg (2008) CrossRef
12.
Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Upper Saddle River (1998)MATH
13.
Huang, W.L., Peleska, J., Schulze, U.: Contract Support for Evolving SoS. Public Document D34.3, COMPASS (2014)
14.
Liu, Z., Jifeng, H., Li, X.: rCOS: refinement of component and object systems. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 183–221. Springer, Heidelberg (2005) CrossRef
15.
Miyazawa, A., Lima, L., Cavalcanti, A.: Formal models of SysML blocks. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 249–264. Springer, Heidelberg (2013) CrossRef
16.
Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: A UTP semantics for \({\sf Circus}\). FACJ 21(1–2), 3–32 (2009)
17.
Peleska, J.: Translating testing theories for concurrent systems. In: Correct System Design, Essays Dedicated to Ernst-Rüdiger Olderog on the Occasion of his 60th Birthday, LNCS. Springer (2015)
18.
Roscoe, A.W. (ed.): A Classical Mind: Essays in Honour of C. A. R. Hoare. Prentice Hall International (UK) Ltd., Hertfordshire (1994)
19.
Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, London (2011) MATH
20.
Sherif, A., Cavalcanti, A.L.C., He, J., Sampaio, A.C.A.: A process algebraic framework for specification and validation of real-time systems. FACJ 22(2), 153–191 (2010)MATH
21.
Zeyda, F., Santos, T., Cavalcanti, A., Sampaio, A.: A modular theory of object orientation in higher-order UTP. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 627–642. Springer, Heidelberg (2014) CrossRef
22.
Zhu, H., He, J., Qin, S., Brooke, P.: Denotational semantics and its algebraic derivation for an event-driven system-level language. FACJ 27(1), 133–166 (2015)MathSciNetMATH
Metadaten
Titel
CSP and Kripke Structures
verfasst von
Ana Cavalcanti
Wen-ling Huang
Jan Peleska
Jim Woodcock
Copyright-Jahr
2015
Buch
Theoretical Aspects of Computing - ICTAC 2015

Print ISBN: 978-3-319-25149-3

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

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-25150-9_29

Premium Partner

    Bildnachweise