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

DOI10.1007/978-3-031-30826-0_2MaRDI QIDQ6535218zbMATH OpenFDO

Authors Leandro Batista Ribeiro, Florian Lorber, Ulrik Nyman, Kim G. Larsen, Marcel Baunach

Publication date 24 November 2023

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-30826-0_2

zbMATH Keywords

embedded systemsformal methodsreal-time operating systemssoftware compositionUppaal

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

• Toward compositional verification of interruptible OS kernels and device drivers
• Operating system task management requirements layer modeling and verification based on Coq
• On the correctness of upper layers of automotive systems
• Applying formal verification to an open-source real-time operating system
• scientific article; zbMATH DE number 1751915

Cites work

• Dafny: an automatic program verifier for functional correctness
• Deep specifications and certified abstraction layers
• Enabling floating-point arithmetic in the Coq proof assistant
• Formal Methods for the Design of Real-Time Systems
• Formalizing the LLVM intermediate representation for verified program transformations
• scientific article; zbMATH DE number 5613976 (Why is no real title available?)
• scientific article; zbMATH DE number 1759608 (Why is no real title available?)
• Modeling in Event B. System and software engineering.
• Operating system verification---an overview
• Uppaal in a nutshell
• Urgent Partial Order Reduction for Extended Timed Automata
• Using formal reasoning on a model of tasks for FreeRTOS

Cited in

(3)

• A compositional behavioral modeling framework for embedded system design and conformance checking
• Applying formal verification to an open-source real-time operating system
• Towards applying the composition principle to verify a microkernel operating system

This page was built for publication: A modeling concept for formal verification of OS-based compositional software

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