| Title | Analysis of three hybrid systems in time $μ$ {CRL} |
| Publication Type | Book Chapter |
| Year of Publication | 1998 |
| Authors | Groote J F, van Wamel JJ |
| Book Title | 1000 |
| Pagination | 24 |
| Publisher | Centrum voor Wiskunde en Informatica (CWI) |
| City | ISSN 1386-369X |
| Keywords | Hybrid systems, parallelism, Process Algebra, timed $μ$CRL |
| Abstract | We study three simple hybrid control systems in timed $μ$CRL \cite{Gr97}. A temperature regulation system, a bottle filling system and a railway gate control system are specified component-wise and expanded to linear process equations. Some basic properties of the systems are analysed and a few correctness requirements are proven to be satisfied. Although not designed for this purpose, timed $μ$CRL seems to allow detailed analysis and verification of hybrid systems. The operators for parallelism and encapsulation are handled using some basic results from \cite{GvW98}. It turns out that the expansion and encapsulation of a parallel composition of processes generally leads to a considerable number of potential ıt time deadlocks\/}, which generally turn out to be harmless. Also inherent to parallelism are the multiple time dependencies between the summands of the separate components. As a consequence, expansions tend to lead to large numbers of terms. Various techniques, such as the use of invariants \cite{BG94}, have to be employed to master these complications. |
| URL | http://www.cwi.nl/ftp/CWIreports/SEN/SEN-R9815.ps.Z |