Applying formal verification to an open-source real-time operating system

DOI10.1007/978-3-031-40436-8_13zbMATH Open1547.68107MaRDI QIDQ6535839

Frédéric Tuong, Andrew Butterfield

Publication date: 28 February 2024

zbMATH Keywords

model checkingtest generationreal-time operating systemsunifying theories of programmingPromela/SPINRTEMS

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Mutation testing in UTP
• Unifying theories of reactive design contracts
• Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
• From LCF to Isabelle/HOL
• A testing perspective on algebraic, denotational, and operational semantics
• On the Relationship between LTL Normal Forms and Büchi Automata
• Transaction Calculus
• UTP and Temporal Logic Model Checking
• A Note on Traces Refinement and the conf Relation in the Unifying Theories of Programming
• Unifying Theories of Locations
• Unifying Input Output Conformance
• Guarded commands, nondeterminacy and formal derivation of programs
• UTCP: Compositional Semantics for Shared-Variable Concurrency
• Testing can be formal, too
• Pointers and Records in the Unifying Theories of Programming

This page was built for publication: Applying formal verification to an open-source real-time operating system