- 【Updated on May 12, 2025】 Integration of CiNii Dissertations and CiNii Books into CiNii Research
- Trial version of CiNii Research Automatic Translation feature is available on CiNii Labs
- Suspension and deletion of data provided by Nikkei BP
- Regarding the recording of “Research Data” and “Evidence Data”
Model checking of control-finite CSP programs
Description
The authors investigate an automatic verification mechanism for control-finite communicating sequential processes (CSP) programs by using the model checking technique. CSP programs with variables and usual sequential constructs are transformed into transition systems to apply the model checking technique. More specifically, binding of variables are attached to states and sequential statements are treated uniformly as events in a parallel environment. With this transformation, the system can be viewed as implementing the model checker for a static version of value-passing CCS. Another characteristic of the system is that the CSP programs to be verified are not limited to finite-state, but can be control-finite, CSP programs are control-finite if their control flow is finite. The model checker was implemented and various examples of parallel programming were verified. >
Journal
-
- [1993] Proceedings of the Twenty-sixth Hawaii International Conference on System Sciences
-
[1993] Proceedings of the Twenty-sixth Hawaii International Conference on System Sciences ii 174-183, 2002-12-31
IEEE
