A Static Analysis of Strongly Synchronous System

• Main Authors: Li Wang, 王立
• Other Authors: Bal Wang
• Format: Others
• Language: zh-TW
• Published: 1993
• Online Access: http://ndltd.ncl.edu.tw/handle/10429272056858293865

碩士 === 淡江大學 === 資訊工程研究所 === 81 === Several approaches have been proposed in study of communica- ting concurrent systems , such as asynchronous models : Petri- Nets , CSP , CCS ,and synchronous models : Esterel , Statecharts , Lustre and Signal . One significant implementation upon those models is to design reactive systems , e.g. , nuclear power sys- tems , flight control systems , etc , react to external stimuli (signals) continuously and never terminate . There are some problems for such embedded systems to face , for instance , nondeterminism (output signals could compete with concurrent input signals) , blowing-up states (in parallelism) . One of the approaches to solve the nondeterminism problem is to assume that reactions are instantaneous and atomic . This as- sumption is referred to as strong synchrony assumption . To achieve such a goal , we can simply assume that every ac- tion does not take time . Under this assumption , the relation between stimuli and reactions become clear and deterministic . Moreover , declaration of incompatable relations(mutually exclu- sive relations) over signals and local signals together with st- rong synchrony assumption can greatly reduce the number of sta- tes in solving state explosion problem . Based on strong synchrony assumption and declaration of state reduction relations over signals , we present a static analysis to translate a synchronous program written in Esterel into a de- sired sequential deterministic finite automaton (DFA). To arrive such a goal , a set of computable conditions is explored and a corresponding algorithm is given to merge DFAs of sequential mo- dules which are parallelly composed into a DFA for the whole sy- stem such that the resulted DFA can run on a single processor and leads to the same results of strong synchrony assumption as the machine runs infinitely fast . Finally , the implementation and analysis of the algorithm is also given in the thesis .