Verifiable Code Generation from Scheduled Event-B Models

DOI10.1007/978-3-319-91271-4_16MaRDI QIDQ5881452zbMATH OpenOpenAlexFDO

Authors

Publication date 10 March 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-91271-4_16

Mathematics Subject Classification ID

Distributed systems (68M14) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Theory of programming languages (68N15)

Recommendations

• Experiments in program verification using Event-B
• Modeling numerical programs with Event-B
• Derivation of concurrent programs by stepwise scheduling of Event-B models
• Schedulability verification of embedded system AADL model based on timed automata
• Verifying a scheduling protocol of safety-critical systems

Cites work

• Dafny: an automatic program verifier for functional correctness
• Distributed cooperation with action systems
• scientific article; zbMATH DE number 108549 (Why is no real title available?)
• Modeling in Event B. System and software engineering.
• On the Purpose of Event-B Proof Obligations

Cited in

(1)

• scientific article; zbMATH DE number 7453194 (Why is no real title available?)

Describes a project that uses

Uses Software

• Rodin
• Dafny
• Boogie
• Eiffel
• z3

This page was built for publication: Verifiable Code Generation from Scheduled Event-B Models

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