Operating system task management requirements layer modeling and verification based on Coq

DOI10.13328/J.CNKI.JOS.005961MaRDI QIDQ3386299zbMATH OpenFDO

Authors

Publication date 14 January 2021

zbMATH Keywords

task managementformal verificationformal modelingrequirement layer

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Using formal reasoning on a model of tasks for FreeRTOS
• Formal memory models for the verification of low-level operating-system code
• Verifying safety critical task scheduling systems in PPTL axiom system
• Satellite rendezvous and conjunction avoidance: case studies in verification of nonlinear hybrid systems
• Formal verification of multitasking applications based on timed automata model

Cited in

(3)

• scientific article; zbMATH DE number 2011465 (Why is no real title available?)
• A modeling concept for formal verification of OS-based compositional software
• Using formal reasoning on a model of tasks for FreeRTOS

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Operating system task management requirements layer modeling and verification based on Coq

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