A process algebraic framework for specification and validation of real-time systems
DOI10.1007/S00165-009-0119-6zbMATH Open1214.68224OpenAlexW1998976523MaRDI QIDQ968306FDOQ968306
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
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- Uppaal in a nutshell
- A theory of timed automata
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A timed model for communicating sequential processes
- Unifying theories for logic programming
- A calculus of durations
- Title not available (Why is that?)
- A brief history of Timed CSP
- Title not available (Why is that?)
- A refinement strategy for Circus
- FM 2005: Formal Methods
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theoretical Aspects of Computing - ICTAC 2004
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (22)
- Laws of mission-based programming
- A Unary Semigroup Trace Algebra
- Unifying theories of reactive design contracts
- Title not available (Why is that?)
- Title not available (Why is that?)
- Circus Time with Reactive Designs
- Modelling temporal behaviour in complex systems with Timebands
- From control law diagrams to Ada via \textsf{Circus}
- An engineering process for the verification of real-time systems
- Test-data generation for control coverage by proof
- An Axiomatic Value Model for Isabelle/UTP
- Denotational semantics and its algebraic derivation for an event-driven system-level language
- Towards Algebraic Semantics of Circus Time
- TPAP: an algebra of preemptive processes for verifying real-time systems with shared resources
- Simulink Timed Models for Program Verification
- Theoretical Aspects of Computing - ICTAC 2004
- A Stepwise Approach to Linking Theories
- Safety-critical Java programs from \textsf{Circus} models
- The safety-critical Java memory model formalised
- A specification theory of real-time processes
- Jifeng He at Oxford and beyond: an appreciation
- Automated verification of reactive and concurrent programs by calculation
Uses Software
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)
