Automatic Verification of Bossa Scheduler Properties

DOI10.1016/J.ENTCS.2007.05.026MaRDI QIDQ5178992zbMATH OpenOpenAlexWikidataFDO

Authors Jean-Paul Bodeveix, Mamoun Filali, Julia L. Lawall, Gilles Muller

Publication date 18 March 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2007.05.026

zbMATH Keywords

model checkingschedulingrefinementWS1S

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Recommendations

• Verification of schedulability for real-time programs
• Automatable verification of sequential consistency
• Verification of a fieldbus scheduling protocol using timed automata
• scientific article; zbMATH DE number 1497853
• Publication:4490726
• Automatic verification for a class of distributed systems
• Automatic and hierarchical verification for concurrent systems
• Automated Verification of Concurrent Search Structures

Cites work

• scientific article; zbMATH DE number 1629942 (Why is no real title available?)
• scientific article; zbMATH DE number 46872 (Why is no real title available?)
• scientific article; zbMATH DE number 1223628 (Why is no real title available?)
• scientific article; zbMATH DE number 557977 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• Comments on Always-true is not invariant: Assertional reasoning about invariance
• Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment
• The B-Book

Describes a project that uses

Uses Software

• MONA
• UNITY
• FAST

This page was built for publication: Automatic Verification of Bossa Scheduler Properties

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