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

DOI10.1007/978-3-031-30826-0_2zbMATH Open1541.68212MaRDI QIDQ6535218

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

Publication date: 24 November 2023

zbMATH Keywords

embedded systemsformal methodsreal-time operating systemsUppaalsoftware composition

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
• Using formal reasoning on a model of tasks for FreeRTOS
• Operating system verification---an overview
• Uppaal in a nutshell
• Deep Specifications and Certified Abstraction Layers
• Formalizing the LLVM intermediate representation for verified program transformations
• Dafny: An Automatic Program Verifier for Functional Correctness
• Formal Methods for the Design of Real-Time Systems
• Enabling floating-point arithmetic in the Coq proof assistant
• Urgent Partial Order Reduction for Extended Timed Automata

Related Items (1)

A compositional behavioral modeling framework for embedded system design and conformance checking

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