@inproceedings{morris:2020:abz,
    author="Morris, Karla
        and Snook, Colin
        and Hoang, Thai Son
        and Hulette, Geoffrey
        and Armstrong, Robert
        and Butler, Michael",
    editor="Raschke, Alexander
        and M{\'e}ry, Dominique
        and Houdek, Frank",
    title="Refinement and Verification of Responsive Control Systems",
    booktitle="Rigorous State-Based Methods",
    year="2020",
    publisher="Springer International Publishing",
    address="Cham",
    pages="272--277",
    abstract="Statechart notations with `run to completion' semantics, are popular with engineers for designing controllers that respond to events in the environment with a sequence of state transitions. However, they lack formal refinement and rigorous verification methods., on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. We introduce a notion of refinement into a `run to completion' statechart modelling notation, and leveragetool support for theorem proving. We describe the difficulties in translating `run to completion' semantics intorefinements and suggest a solution. We outline how safety and liveness properties could be verified.",
    isbn="978-3-030-48077-6"
}