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

DOI10.13328/J.CNKI.JOS.005961zbMATH Open1463.68015MaRDI QIDQ3386299FDOQ3386299

Authors:

Publication date: 14 January 2021

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

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)

Cited In (3)

• Title not available (Why is that?)
• A modeling concept for formal verification of OS-based compositional software
• Using formal reasoning on a model of tasks for FreeRTOS

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)