A process algebraic framework for specification and validation of real-time systems

DOI10.1007/S00165-009-0119-6MaRDI QIDQ968306zbMATHOpenAlexFDO

Authors Adnan Sherif, Ana Cavalcanti, He Jifeng, Augusto Sampaio

Publication date 5 May 2010

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

Full work available at URL https://doi.org/10.1007/s00165-009-0119-6

zbMATH Keywords

CSPGalois connectionsrelational modelsunifying theories of programming

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Theoretical Aspects of Computing - ICTAC 2004
• A refinement-based process algebra for timed automata
• Specification and Proof in Real Time CSP
• Towards Algebraic Semantics of Circus Time
• scientific article; zbMATH DE number 1693544

Cites work

• scientific article; zbMATH DE number 1693437 (Why is no real title available?)
• scientific article; zbMATH DE number 1693544 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• scientific article; zbMATH DE number 1949640 (Why is no real title available?)
• scientific article; zbMATH DE number 1487746 (Why is no real title available?)
• scientific article; zbMATH DE number 1519981 (Why is no real title available?)
• A brief history of Timed CSP
• A calculus of durations
• A refinement strategy for Circus
• A theory of timed automata
• A timed model for communicating sequential processes
• FM 2005: Formal Methods
• Theoretical Aspects of Computing - ICTAC 2004
• Unifying theories for logic programming
• Uppaal in a nutshell

Cited in

(24)

• An Axiomatic Value Model for Isabelle/UTP
• Automated verification of reactive and concurrent programs by calculation
• Safety-critical Java programs from \textsf{Circus} models
• The safety-critical Java memory model formalised
• Denotational semantics and its algebraic derivation for an event-driven system-level language
• Laws of mission-based programming
• Towards Algebraic Semantics of Circus Time
• An engineering process for the verification of real-time systems
• TPAP: an algebra of preemptive processes for verifying real-time systems with shared resources
• Modelling temporal behaviour in complex systems with Timebands
• Test-data generation for control coverage by proof
• scientific article; zbMATH DE number 1949640 (Why is no real title available?)
• scientific article; zbMATH DE number 1693544 (Why is no real title available?)
• A stepwise approach to linking theories
• Circus Time with Reactive Designs
• From control law diagrams to Ada via \textsf{Circus}
• A Unary Semigroup Trace Algebra
• A specification theory of real-time processes
• Integrating time and resource into Circus
• Theoretical Aspects of Computing - ICTAC 2004
• An algebraic framework for developing and maintaining real-time systems
• Unifying theories of reactive design contracts
• Jifeng He at Oxford and beyond: an appreciation
• Simulink timed models for program verification

Describes a project that uses

Uses Software

• Rabbit
• Uppaal
• ProofPower
• Z
• Circus

This page was built for publication: A process algebraic framework for specification and validation of real-time systems

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