Prototyping and formal analysis of concurrent and distributed systems

摘要

The author sketches the specification language SEGRAS and illustrates related formal validation techniques with a few simple examples including a dynamic reconfiguration problem. The language is particularly suited for concurrent and distributed applications. It draws from two main sources: algebraic specifications of abstract data types and a special class of high-level Petri nets. The language is supported by an experimental specification environment whose semantic tools exploit the operational semantics of the language.