An algebraic theory for behavioral modeling and protocol synthesis in system design. (English) Zbl 1099.68501

Summary: The design productivity gap has been recognized by the semiconductor industry as one of the major threats to the continued growth of system-on-chips and embedded systems. Ad-hoc system-level design methodologies, that lifts modeling to higher levels of abstraction, and the concept of intellectual property, that promotes reuse of existing components, are essential steps to manage design complexity. However, the issue of compositional correctness arises with these steps. Given components from different manufacturers, designed with heterogeneous models, at different levels of abstraction, assembling them in a correct-by-construction manner is a difficult challenge. We address this challenge by proposing a process algebraic model to support system design with a formal model of computation and serve as a type system to capture the behavior of system components at the interface level. The proposed algebra is conceptually minimal, equipped with a formal semantics defined in a synchronous model of computation. It supports a scalable notion and a flexible degree of abstraction. We demonstrate its benefits by considering the type-based synthesis of latency-insensitive protocols, showing that the synthesis of component wrappers can be optimized by behavioral information carried by interface type descriptions and yield minimized stalls and maximized throughput.


68M07 Mathematical problems of computer architecture
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
Full Text: DOI Link


[1] Amagbegnon TP, Besnard L, Le Guernic P (1995) Implementation of the data-flow synchronous language Signal. In Conference on Programming Language Design and Implementation. ACM Press
[2] Benveniste A, Caspi P, Carloni LP, Sangiovanni-Vincentelli AL (2003) Heterogeneous Reactive Systems Modeling and Correct-by-Construction Deployment. In: Embedded Software Conference. Lecture Notes in Computer Science, Springer Verlag
[3] Benveniste A, Caspi P, Le Guernic P, Marchand H, Talpin J-P, Tripakis S (2002) A protocol for loosely time-triggered architectures. In: Embedded Software Conference. Lecture Notes in Computer Science, Springer Verlag · Zbl 1027.68762
[4] Buck JT, Ha S, Lee E, Messerschmitt D (1994) Ptolemy: A Framework for Simulating and Prototyping Heterogeneous Systems. Int J Comp Simul 4:155–182.
[5] Carloni LP, McMillan KL, Sangiovanni-Vincentelli AL (1999) Latency-insensitive protocols. In: Proceedings of the 11th. International Conference on Computer-Aided Verification. Lecture notes in computer science v. 1633. Springer Verlag · Zbl 1046.68585
[6] Dijkstra E (1976) A Discipline of programming. Prentice Hall · Zbl 0368.68005
[7] De Alfaro L, Henzinger TA (2001) Interface theories for component-based design. Int Workshop on Embedded Software. Lecture Notes in Computer Science v. 2211. Springer-Verlag
[8] Hoare C (1985) Communicating sequential processes. Prentice Hall · Zbl 0637.68007
[9] Hoe J, Arvind (2000) Synthesis of operation-centric hardware descriptions. Proceedings of International Conference on Computer Aided Design. IEEE Press
[10] Kahn G (1974) The semantics of a simple language for parallel programming. In Ifip Congress. North Holland · Zbl 0299.68007
[11] Lee E, Sangiovanni-Vincentelli A (1998) A framework for comparing models of computation. IEEE transactions on computer-aided design, 12. IEEE Press, vol. 17, no.
[12] Le Guernic P, Talpin J-P, Le Lann J-L (2002) Polychrony for system design. In Journal of Circuits, Systems and Computers. Special Issue on Application-Specific Hardware Design. World Scientific
[13] Nowak D, Talpin J-P, Le Guernic P (1999) Synchronous structures. In International Conference on Concurrency Theory. Lecture Notes in Computer Science, Springer Verlag · Zbl 0940.68016
[14] Pnueli A, Shankar N, Singerman E (1998) Fair synchronous transition systems and their liveness proofs. International School and Symposium on Formal Techniques in Real-time and Fault-tolerant Systems. Lecture Notes in Computer Science v. 1468. Springer Verlag
[15] Polychrony: http://www.irisa.fr/espresso/Polychrony, 2004.
[16] Talpin J-P, Le Guernic P, Shukla S, Gupta R, Doucet F (2003) Polychrony for formal refinement-checking in a system-level design methodology. Application of Concurrency to System Design. IEEE Press
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.