English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Over the last several years the tools used for model checking have becomemore efficient and usable. This has enabled users to apply model checking toindustrial-scale problems, however the task of validating the implementation ofthe model is usually much harder. In this paper we present an approach to doend to end verification and validation of a real time system using the SPINmodel checker. Taking the example of the cardiac pacemaker system proposed inthe SQRL Pacemaker Formal Methods Challenge we demonstrate our framework bybuilding a formal model for the cardiac pacemaker in SPIN, checking fordesirable temporal properties of the model (expressed as LTL formulas),generating C code from the model (by refinement of PROMELA) and validating thegenerated implementation (using SPIN). We argue that a state of the art modelchecking tool like SPIN can be used to do formal specification as well asvalidation of the implementation. To evaluate our approach we show that ourpacemaker model is expressive enough to derive consistent operating modes andthat the refinement rules preserve LTL properties.

End to End Verification and Validation with SPIN