Formal Models for Communication-Based Design

Concurrency is an essential element of abstract models for embedded systems. Correctness and e ciency of the design depend critically on the way concurrency is formalized and implemented. Concurrency is about communicating processes. We introduce an abstract formal way of representing communication among processes and we show how to re ne this representation towards implementation. To this end, nt a formal model, Abstract Co-design Finite State Machines ACFSM, and its re nement, Extended Co-design Finite State MaECFSM, developed to capture abstract behavior of concurrent processes and derived from a model Co-design Finite State Machine CFSM we have used in POLIS, a system for the design and veri cation of embedded systems. The design of communication protocols is presented as an example of the use of these formal models.

• Type: Conference
• Year: 2000
• Where: CONCUR
• Authors: Alberto L. Sangiovanni-Vincentelli, Marco Sgroi, Luciano Lavagno
• Keywords: Abstract Co-design Finite, Co-design Finite State, CONCUR 2000, Distributed And Parallel Computing, Finite State Machine