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

DOI10.1007/S00165-009-0119-6zbMath1214.68224OpenAlexW1998976523MaRDI QIDQ968306

Augusto Sampaio, He Jifeng, Adnan Sherif, Ana Cavalcanti

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

CSPrelational modelsGalois connectionsunifying 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)

Related Items (16)

Circus Time with Reactive Designs ⋮ A Unary Semigroup Trace Algebra ⋮ Jifeng He at Oxford and beyond: an appreciation ⋮ The safety-critical Java memory model formalised ⋮ Denotational semantics and its algebraic derivation for an event-driven system-level language ⋮ A Stepwise Approach to Linking Theories ⋮ An Axiomatic Value Model for Isabelle/UTP ⋮ From control law diagrams to Ada via \textsf{Circus} ⋮ Safety-critical Java programs from \textsf{Circus} models ⋮ Modelling temporal behaviour in complex systems with Timebands ⋮ Unifying theories of reactive design contracts ⋮ Test-data generation for control coverage by proof ⋮ Automated verification of reactive and concurrent programs by calculation ⋮ Towards Algebraic Semantics of Circus Time ⋮ Simulink Timed Models for Program Verification ⋮ Laws of mission-based programming

Uses Software

• Rabbit
• Uppaal
• ProofPower
• Z
• Circus

Cites Work

• A brief history of Timed CSP
• A refinement strategy for Circus
• A timed model for communicating sequential processes
• A calculus of durations
• A theory of timed automata
• Uppaal in a nutshell
• Theoretical Aspects of Computing - ICTAC 2004
• FM 2005: Formal Methods
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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