Formalization and correctness of the PALS architectural pattern for distributed real-time systems

DOI10.1016/J.TCS.2012.05.040zbMATH Open1284.68073OpenAlexW2077349223MaRDI QIDQ714796FDOQ714796

José Meseguer, Peter Csaba Ölveczky

Publication date: 11 October 2012

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2012.05.040

Recommendations

• Hybrid multirate PALS
• SMT-based analysis of virtually synchronous distributed hybrid systems
• Pervasive verification of distributed real-time systems
• Modular abstractions for verifying real-time distributed systems
• A TLA+ Formal Specification and Verification of a New Real-Time Communication Protocol

zbMATH Keywords

model checkingrewriting logicsynchronizersdistributed real-time systemsformally verified architectural patterns

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07) Network design and communication in computer systems (68M10) Distributed systems (68M14)

Cites Work

• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Specification of real-time and hybrid systems in rewriting logic
• Title not available (Why is that?)
• Complexity of network synchronization
• Correct-by-construction asynchronous implementation of modular synchronous specifications
• Time, clocks, and the ordering of events in a distributed system
• Title not available (Why is that?)
• Conditional rewriting logic as a unified model of concurrency
• Equational rules for rewriting logic
• Semantic foundations for generalized rewrite theories
• Title not available (Why is that?)
• Semantics and pragmatics of real-time maude
• Title not available (Why is that?)
• Title not available (Why is that?)
• Implementing Synchronous Models on Loosely Time Triggered Architectures
• Formalization and correctness of the PALS architectural pattern for distributed real-time systems

Cited In (5)

• Building correct-by-construction systems with formal patterns
• Formalization and correctness of the PALS architectural pattern for distributed real-time systems
• Hybrid Multirate PALS
• Programming and symbolic computation in Maude
• A relaxation of Üresin and Dubois' asynchronous fixed-point theory in Agda

Uses Software

• Maude

This page was built for publication: Formalization and correctness of the PALS architectural pattern for distributed real-time systems

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