Model checking RAISE applicative specifications

DOI10.1007/S00165-011-0217-0MaRDI QIDQ470000zbMATH OpenOpenAlexFDO

Authors Chris George, Juan Perna

Publication date 11 November 2014

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/10915/22134

zbMATH Keywords

applicative specificationsmodel checkingRAISE

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Applicative Modelling with RAISE
• Model Checking LTL Formulae in RAISE with FDR
• scientific article; zbMATH DE number 1633145
• scientific article; zbMATH DE number 2080188
• scientific article; zbMATH DE number 910719

Cites work

• An algebraic approach to compiler design
• Computer Aided Verification
• FM 2005: Formal Methods
• Hardware and software, verification and testing. Second international Haifa verification conference, HVC 2006, Haifa, Israel, October 23--26, 2006. Revised selected papers
• scientific article; zbMATH DE number 1633145 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 42431 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• scientific article; zbMATH DE number 1956470 (Why is no real title available?)
• scientific article; zbMATH DE number 2172805 (Why is no real title available?)
• scientific article; zbMATH DE number 2102731 (Why is no real title available?)
• scientific article; zbMATH DE number 910719 (Why is no real title available?)
• Model Checking LTL Formulae in RAISE with FDR
• Model checking RAISE applicative specifications
• Real-time systems development with duration calculi: an overview.
• Symbolic model checking: \(10^{20}\) states and beyond
• The B-Book
• ZB 2005: Formal Specification and Development in Z and B

Cited in

(4)

• Stepwise development and model checking of a distributed interlocking system using RAISE
• Stepwise development and model checking of a distributed interlocking system -- using RAISE
• Applicative Modelling with RAISE
• Model checking RAISE applicative specifications

Describes a project that uses

Uses Software

• RAISE
• PROMELA
• SPIN
• ProB
• Java PathFinder
• Bandera
• Z
• SLAM
• NuSMV

This page was built for publication: Model checking RAISE applicative specifications

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