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.
CITATION STYLE
Alberto Sangiovanni-Vincentelli, Marco Sgroi, L. L. (2000). CONCUR 2000 — Concurrency Theory. (C. Palamidessi, Ed.) (Vol. 1877, pp. 29–47). Berlin, Heidelberg: Springer Berlin Heidelberg. Retrieved from http://link.springer.com/chapter/10.1007/3-540-44618-4_4
Mendeley helps you to discover research relevant for your work.