Modeling and Verifying Concurrent Programs with Finite Chu Spaces |
| |
| Authors: | Xu-Tao Du Chun-Xiao Xing Li-Zhu Zhou |
| |
| Affiliation: | 1.Department of Computer Science and Technology,Tsinghua University,Beijing,China;2.Research Institute of Information Technology,Tsinghua University,Beijing,China |
| |
| Abstract: | Finite Chu spaces are proposed for the modeling and verification of concurrent programs. In order to model not only typical
concurrent behaviors but also modern exception handling and synchronization mechanisms, we design an enriched process algebra
of Chu spaces from a practical point of view. To illustrate the power of finite Chu spaces and the process algebra while abstracting
away from language-specific details, an imaginary concurrent programming language (ICL) is designed. A denotational semantics
of ICL is presented using finite Chu spaces and the enriched process algebra. The valuation functions are fairly straightforward
since the carefully designed operators have done much of the job. The enriched process algebra is also used as the specification
language for Chu spaces, with which process-algebraic properties can be specified. Verification algorithms are presented with
their time complexities discussed. |
| |
| Keywords: | |
| 本文献已被 万方数据 SpringerLink 等数据库收录！ |
|
