Formal Models for Communication-Based Design

Lecture notes in computer sciencePublished 1 January 2000

Alberto Sangiovanni‐Vincentelli, Marco Sgroi, Luciano Lavagno

DOI10.1007/3-540-44618-4_4

Source URL

Citations31

SJR quartileQ2

SJR score0.35

SNIP0.55

TL;DR

This work introduces an abstract formal way of representing communication among processes and shows how to refine this representation towards implementation, developed to capture abstract behavior of concurrent processes.

Abstract

Concurrency is an essential element of abstract models for embedded systems. Correctness and efficiency 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 refine this representation towards implementation. To this end, we present a formal model, Abstract Co-design Finite State Machines (ACFSM), and its refinement, Extended Co-design Finite State Machines (ECFSM), 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 verification of embedded systems. The design of communication protocols is presented as an example of the use of these formal models.

Keywords

Computer Science

IFIP CongressThe Semantics of a Simple Language for Parallel Programming.

2,116 Citations1974Gilles Kahn

A simple language for parallel programming is described and its mathematical properties are studied to make a case for more formal languages for systems programming and the design of operating systems.

Proceedings of the IEEESynchronous data flow

1,802 Citations1987Edward A. Lee, David G. Messerschmitt

A preliminary SDF software system for automatically generating assembly language code for DSP microcomputers is described, and two new efficiency techniques are introduced, static buffering and an extension to SDF to efficiently implement conditionals.

Elsevier eBooksPtolemy: A Framework for Simulating and Prototyping Heterogeneous Systems

991 Citations2002Joseph Buck, Soonhoi Ha +2 more

Ptolemy is an environment for simulation and prototyping of heterogeneous systems that uses modern object-oriented software technology (C++) to model each subsystem in a natural and efficient manner, and to integrate these subsystems into a whole.

IEEE Transactions on Computer-Aided Design of Integrated Circuits and SystemsA framework for comparing models of computation

689 Citations1998Edward A. Lee, Alberto Sangiovanni‐Vincentelli

A denotational framework (a "meta model") within which certain properties of models of computation can be compared is given, which describes concurrent processes in general terms as sets of possible behaviors.

Hardware-Software Co-Design of Embedded Systems

601 Citations1997Felice Balarin, Massimiliano Chiodo +9 more

This paper is intended to give a complete overview of the POLIS system including its formal and algorithmic aspects and will be of interest to embedded system designers (automotive electronics, consumer electronics and telecommunications), micro-controller designers, CAD developers and students.

Hardware-software co-design of embedded systems: the POLIS approach

543 Citations1997Felice Balarin, Massimiliano Chiodo +9 more

Interface-based design

289 Citations1997J.A. Rowson, Alberto Sangiovanni‐Vincentelli

A new system design methodology is proposed that separates communication from behavior and the potential for this methodology to improve verification, modelling and synthesis is explored.

Automatic synthesis of interfaces between incompatible protocols

167 Citations1998Roberto Passerone, J.A. Rowson +1 more

This work proposes using regular expression based protocol descriptions to show how to map the message onto a signaling protocol, given two protocols, and proposes an algorithm to build an interface machine.

View PDF

Synthesis of embedded software using free-choice Petri nets

89 Citations1999Marco Sgroi, Luciano Lavagno +2 more

A Quasi-Static Scheduling (QSS) algorithm that generates a schedule in which run-time decisions are made only for data-dependent control structures, and it is shown how to synthesize from a quasi-static schedule a C code implementation that consists of a set of concurrent tasks.

View PDF

Designing wireless protocols: methodology and applications

34 Citations2002Marco Sgroi, J.L. da Silva +4 more

A new design methodology for wireless protocols based on the principle of orthogonalization of concerns is presented, which separates function and architecture design and emphasizes the use of formal models to ensure correctness and reduce design time.