Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6875255 | Science of Computer Programming | 2018 | 24 Pages |
Abstract
A case study centred on a fuel supply system for a small aircraft is presented in Hybrid Event-B, an extension of conventional Event-B that allows for the modelling and verification of hybrid and cyberphysical systems exhibiting nontrivial continuous behaviour. In contrast to many such case studies, which concentrate predominantly on timing issues, the focus in the present work is on nontrivial physical behaviour, and on the effect that this has on various refinement and partition strategies. More liberal proof obligations are developed to add flexibility to the decomposition process.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Richard Banach,