Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

13.02.2017 | Theme Section Paper

Synthesis of verifiable concurrent Java components from formal models

Zeitschrift:
Software & Systems Modeling
Autoren:
Julio Mariño, Raúl N. N. Alborodo, Lars-Åke Fredlund, Ángel Herranz
Wichtige Hinweise
Communicated by Dr. F. Ciccozzi, J. Carlson, P. Pelliccione, and M. Tivoli.

Abstract

Concurrent systems are hard to program, and ensuring quality by means of traditional testing techniques is often very hard as errors may not show up easily and reproducing them is hard. In previous work, we have advocated a model-driven approach to the analysis and design of concurrent, safety-critical systems. However, to take full advantage of these techniques, they must be supported by code generation schemes for concrete programming languages. Ideally, this translation should be traceable, automated and should support the verification of the generated code. In our work, we consider the problem of generating a concurrent Java component from a high-level model of inter-process interaction (i.e., communication + synchronization). We call our formalism shared resources. From the model, which can be represented in mathematical notation or written as a Java interface annotated using an extension of JML, a Java component can be obtained by a semiautomatic translation. We describe how to obtain shared memory (using a priority monitors library) and message passing (using the JCSP library) implementations. Focusing on inter-process interaction for formal development is justified by several reasons, e.g., mathematical models are language-independent and allow to analyze certain concurrency issues, such as deadlocks or liveness properties prior to code generation. Also, the Java components produced from the shared resource model will contain all the concurrency-related language constructs, which are often responsible for many of the errors in concurrent software. We follow a realistic approach where the translation is semiautomatic (schemata for code generation) and the programmer still retains the power of coding or modifying parts of the code for the resource. The code thus obtained is JML-annotated Java with proof obligations that help with code traceability and verification of safety and liveness properties. As the code thus obtained is not automatically correct, there is still the need to verify its conformance to the original specs. We illustrate the methodology by developing a concurrent control system and verifying the code obtained using the KeY program verification tool. We also show how KeY can be used to find errors resulting from a wrong use of the templates.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit dem Kombi-Abo erhalten Sie vollen Zugriff auf über 1,8 Mio. Dokumente aus mehr als 61.000 Fachbüchern und rund 500 Fachzeitschriften aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit dem Wirtschafts-Abo erhalten Sie Zugriff auf über 1 Mio. Dokumente aus mehr als 45.000 Fachbüchern und 300 Fachzeitschriften aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit dem Technik-Abo erhalten Sie Zugriff auf über 1 Mio. Dokumente aus mehr als 40.000 Fachbüchern und 300 Fachzeitschriften aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Maschinenbau + Werkstoffe

Testen Sie jetzt 30 Tage kostenlos.

Literatur
Über diesen Artikel

Premium Partner

BranchenIndex Online

Die B2B-Firmensuche für Industrie und Wirtschaft: Kostenfrei in Firmenprofilen nach Lieferanten, Herstellern, Dienstleistern und Händlern recherchieren.

Whitepaper

- ANZEIGE -

Best Practices für die Mitarbeiter-Partizipation in der Produktentwicklung

Unternehmen haben das Innovationspotenzial der eigenen Mitarbeiter auch außerhalb der F&E-Abteilung erkannt. Viele Initiativen zur Partizipation scheitern in der Praxis jedoch häufig. Lesen Sie hier  - basierend auf einer qualitativ-explorativen Expertenstudie - mehr über die wesentlichen Problemfelder der mitarbeiterzentrierten Produktentwicklung und profitieren Sie von konkreten Handlungsempfehlungen aus der Praxis.
Jetzt gratis downloaden!

Bildnachweise