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

DOI10.1007/S00165-007-0042-7zbMATH Open1141.68024OpenAlexW1976111119MaRDI QIDQ2481209FDOQ2481209

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

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\)

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)

Cites Work

• Title not available (Why is that?)
• An overview of the runtime verification tool Java PathExplorer
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Theory of Communicating Sequential Processes
• Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker
• Title not available (Why is that?)
• Specification-oriented semantics for communicating processes
• Title not available (Why is that?)
• LSCs: Breathing life into message sequence charts
• A refinement strategy for Circus
• Title not available (Why is that?)
• Relational concurrent refinement
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Concurrency and refinement in the unified modeling language
• Specification and (property) inheritance in CSP-OZ
• How the design of JML accommodates both runtime assertion checking and formal verification
• Title not available (Why is that?)
• Data abstraction techniques in the validation of CSP-OZ specifications
• A discrete-time UML semantics for concurrency and communication in safety-critical applications
• Checking consistency in UML diagrams: classes and state machines.
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (6)

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

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)