Integrating a formal method into a software engineering process with UML and Java

DOI10.1007/S00165-007-0042-7MaRDI QIDQ2481209zbMATH OpenOpenAlexFDO

Authors Ernst-Rüdiger Olderog, Holger Rasch, Heike Wehrheim, Michael Möller

Publication date 9 April 2008

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-007-0042-7

zbMATH Keywords

CSPJavaFormal specificationModel checkingUMLObject-ZContractsModellingRuntime checking

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A formal approach to object-oriented software engineering
• Publication:4509996
• scientific article; zbMATH DE number 1759367
• scientific article; zbMATH DE number 1693515
• Specification, refinement and verification of concurrent systems -- an integration of Object-\(Z\) and \(CSP\)

Cites work

• scientific article; zbMATH DE number 1670567 (Why is no real title available?)
• scientific article; zbMATH DE number 1693430 (Why is no real title available?)
• scientific article; zbMATH DE number 1693515 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 1105469 (Why is no real title available?)
• scientific article; zbMATH DE number 2080013 (Why is no real title available?)
• scientific article; zbMATH DE number 1487740 (Why is no real title available?)
• scientific article; zbMATH DE number 1519981 (Why is no real title available?)
• scientific article; zbMATH DE number 2086954 (Why is no real title available?)
• scientific article; zbMATH DE number 2087132 (Why is no real title available?)
• scientific article; zbMATH DE number 2087419 (Why is no real title available?)
• scientific article; zbMATH DE number 1863159 (Why is no real title available?)
• scientific article; zbMATH DE number 763725 (Why is no real title available?)
• scientific article; zbMATH DE number 1409638 (Why is no real title available?)
• A Theory of Communicating Sequential Processes
• A discrete-time UML semantics for concurrency and communication in safety-critical applications
• A refinement strategy for Circus
• An overview of the runtime verification tool Java PathExplorer
• Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker
• Checking consistency in UML diagrams: classes and state machines.
• Concurrency and refinement in the unified modeling language
• Data abstraction techniques in the validation of CSP-OZ specifications
• How the design of JML accommodates both runtime assertion checking and formal verification
• LSCs: Breathing life into message sequence charts
• Relational concurrent refinement
• Specification and (property) inheritance in CSP-OZ
• Specification-oriented semantics for communicating processes

Cited in

(6)

• Dynamic consistency in process algebra: from paradigm to ACP
• Dynamic consistency in process algebra: from paradigm to ACP
• Model transformations across views
• Automatic verification of combined specifications: an overview
• Integrating formal specifications into applications: the ProB Java API
• Combining the box structure development method and CSP for software development

Describes a project that uses

Uses Software

• SPIN
• Eiffel
• JML
• Bandera
• JPAX
• Z
• FDR2
• Circus
• Jass

This page was built for publication: Integrating a formal method into a software engineering process with UML and Java

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2481209)