A formal framework for modeling and validating simulink diagrams

DOI10.1007/s00165-009-0108-9zbMath1192.68438OpenAlexW2099661188MaRDI QIDQ1037245

Chunqing Chen, Jun Sun, Jin-Song Dong

Publication date: 13 November 2009

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

Full work available at URL: https://ink.library.smu.edu.sg/sis_research/5037

zbMATH Keywords

formal verificationreal-time specificationsimulinkZ language

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items (5)

The refinement calculus of reactive systems ⋮ A contract-based semantics and refinement for Simulink ⋮ A Two-Way Path Between Formal and Informal Design of Embedded Systems ⋮ From control law diagrams to Ada via \textsf{Circus} ⋮ Simulink Timed Models for Program Verification

Uses Software

• PVS
• Simulink
• ClawZ
• Z
• Circus

Cites Work

• A refinement strategy for Circus
• A calculus of durations
• FM 2005: Formal Methods
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A formal framework for modeling and validating simulink diagrams