By the same authors

Proving properties of stateflow models using ISO standard Z and CADIZ

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Author(s)

Department/unit(s)

Publication details

Title of host publicationZB 2005: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, PROCEEDINGS
DatePublished - 2005
Pages104-123
Number of pages20
PublisherSPRINGER-VERLAG BERLIN
Place of PublicationBERLIN
EditorsH Treharne, S King, M Henson, S Schneider
Original languageEnglish
ISBN (Print)3-540-25559-1

Abstract

This paper focuses on the use of ISO Standard Z and CADiZ in the formal validation of Stateflow models against requirements-oriented assumptions. It documents some of what the Simulink/Stateflow Analyser tool does in support of the Practical Formal Specification method. The tool aims to automate the formal validations of the method, so that users of Simulink/Stateflow can benefit from them. The Z exploits some notations that are particular to ISO Standard Z. The automation is aided by quite terse tactics interpreted by CADIZ.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations