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

DOI10.1007/978-3-031-40436-8_13MaRDI QIDQ6535839zbMATH OpenFDO

Authors Andrew Butterfield, Frédéric Tuong

Publication date 28 February 2024

Full work available at URL https://doi.org/10.1007/978-3-031-40436-8_13

zbMATH Keywords

model checkingPromela/SPINreal-time operating systemsRTEMStest generationunifying theories of programming

Mathematics Subject Classification ID

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

Recommendations

• Using formal reasoning on a model of tasks for FreeRTOS
• A modeling concept for formal verification of OS-based compositional software
• scientific article; zbMATH DE number 1693445
• Linear temporal logic symbolic model checking
• How to verify a Safe real-time system: The application of model checking and timed automata to the production cell case study

Cites work

• A note on traces refinement and the conf relation in the unifying theories of programming
• A testing perspective on algebraic, denotational, and operational semantics
• From LCF to Isabelle/HOL
• Guarded commands, nondeterminacy and formal derivation of programs
• scientific article; zbMATH DE number 1949640 (Why is no real title available?)
• scientific article; zbMATH DE number 1759984 (Why is no real title available?)
• scientific article; zbMATH DE number 1852174 (Why is no real title available?)
• Mutation testing in UTP
• On the relationship between LTL normal forms and Büchi automata
• Pointers and Records in the Unifying Theories of Programming
• Testing can be formal, too
• Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
• Transaction calculus (invited paper)
• Unifying input output conformance
• Unifying theories of locations
• Unifying theories of reactive design contracts
• UTCP: Compositional Semantics for Shared-Variable Concurrency
• UTP and temporal logic model checking

Cited in

(1)

• A modeling concept for formal verification of OS-based compositional software

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

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