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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Hard-Wiring CSP Hiding: Implementing Channel Abstraction to Generate Verified Concurrent Hardware Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Refinement Strategies for Safety-Critical Java

verfasst von : Alvaro Miyazawa, Ana Cavalcanti

Erschienen in: Formal Methods: Foundations and Applications

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Safety-Critical Java (SCJ) is a version of Java that supports the development of real-time, embedded, safety-critical software. SCJ introduces abstractions that enforce a simpler architecture, and simpler concurrency and memory models, to support easier certification. In this paper, we detail a refinement strategy that takes a state-rich process algebraic design specification that adheres to a cyclic executive pattern and produces an SCJ design that can be automatically translated to code. We then show how this refinement strategy can be extended to support more complex patterns that include non-terminating and multiple missions.

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 Towards Reasoning in Dynamic Logics with Rewriting Logic: The Petri-PDL Case
Nächstes Kapitel Verifying Transformations of Java Programs Using Alloy
Literatur
1.
2.
Burdy, L., et al.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7(3), 212–232 (2005)CrossRef
3.
Cavalcanti, A., Sampaio, A., Woodcock, J.: Unifying classes and processes. Softw. Syst. Model. 4(3), 277–296 (2005)CrossRef
4.
Cavalcanti, A.L.C., Clayton, P., O’Halloran, C.: From control law diagrams to Ada via Circus. Formal Aspects Comput. 23(4), 465–512 (2011)CrossRefMATH
5.
Cavalcanti, A.L.C., et al.: Safety-Critical Java programs from Circus models. Real-Time Syst. 49(5), 614–667 (2013)CrossRefMATH
6.
Haddad, G., et al.: The design of SafeJML, a specification language for SCJ with supportfor WCET specification. In: JTRES 2010, pp. 155–163. ACM (2010)
7.
Locke, D., et al.: Safety-Critical Java technology specification. Technical report
8.
van Benthem, J.: Reasoning about strategies. In: Coecke, B., Ong, L., Panangaden, P. (eds.) Computation, Logic, Games and Quantum Foundations. LNCS, vol. 7860, pp. 336–347. Springer, Heidelberg (2013)
9.
Miyazawa, A., Cavalcanti, A.: Formal refinement in SysML. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 155–170. Springer, Heidelberg (2014)
10.
11.
Miyazawa, A., Cavalcanti, A.L.C.: Refinement-oriented models of Stateflow charts. Sci. Comput. Program. 77(10–11), 1151–1177 (2012)CrossRefMATH
12.
Miyazawa, A., Cavalcanti, A.L.C.: SCJ-Circus: a refinement-oriented formal notation for Safety-Critical Java. In: Refinement Workshop (2015)
13.
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
14.
Oliveira, M.V.M.: Formal derivation of state-rich reactive programs using Circus. Ph.D. thesis, University of York (2006)
15.
Roscoe, A.W.: Understanding Concurrent Systems: Texts in Computer Science. Springer, London (2011)
16.
Wei, K., Woodcock, J.C.P., Cavalcanti, A.L.C.: Circus Time with Reactive Designs. In: Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.) UTP 2012. LNCS, vol. 7681, pp. 68–87. Springer, Heidelberg (2012)CrossRef
17.
Wellings, A.: Concurrent and Real-Time Programming in Java. Wiley, Hoboken (2004)
18.
Woodcock, J.C.P., Davies, J.: Using Z-Specification, Refinement, and Proof. Prentice-Hall, New York (1996)MATH
19.
Zeyda, F., Cavalcanti, A., Wellings, A., Woodcock, J., Wei, K.: Refinement of the Parallel CDx. Technical report, University of York (2012)
Metadaten
Titel
Refinement Strategies for Safety-Critical Java
verfasst von
Alvaro Miyazawa
Ana Cavalcanti
Copyright-Jahr
2016
Buch
Formal Methods: Foundations and Applications

Print ISBN: 978-3-319-29472-8

Electronic ISBN: 978-3-319-29473-5

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-29473-5_6