Verifying hierarchical Ptolemy II discrete-event models using real-time maude

DOI10.1016/J.SCICO.2010.10.002zbMath1264.68051OpenAlexW2098851201MaRDI QIDQ1951606

Thomas Huining Feng, Kyungmin Bae, Peter Csaba Ölveczky, Stavros Tripakis, Edward A. Lee

Publication date: 6 June 2013

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2010.10.002

zbMATH Keywords

formal semanticsformal verificationmodel checkingrewriting logicPtolemy II DE modelsreal-time maude

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (5)

The rewriting logic semantics project: a progress report ⋮ Twenty years of rewriting logic ⋮ Verifying hierarchical Ptolemy II discrete-event models using real-time maude ⋮ A modular formal semantics for Ptolemy ⋮ Executable rewriting logic semantics of Orc and formal analysis of Orc programs

Uses Software

• JavaFAN
• StateFlow
• Maude
• Ptolemy
• VESTA
• LUSTRE
• MOMENT2

Cites Work

• The rewriting logic semantics project
• Semantics and pragmatics of real-time maude
• CPO semantics of timed interactive actor networks
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Statecharts: a visual formalism for complex systems
• Conditional rewriting logic as a unified model of concurrency
• The semantics and execution of a synchronous block-diagram language.
• Specification of real-time and hybrid systems in rewriting logic
• Equational rules for rewriting logic
• Verifying hierarchical Ptolemy II discrete-event models using real-time maude
• Semantic foundations for generalized rewrite theories
• Abstraction and Completeness for Real-Time Maude
• Actors without Directors: A Kahnian View of Heterogeneous Systems
• On the Behavioral Semantics of Real-Time Domain Specific Visual Languages
• Computer Aided Verification
• Modeling Timed Concurrent Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Verifying hierarchical Ptolemy II discrete-event models using real-time maude