Application of DES Theory to Verification of Software Components
スポンサーリンク
概要
- 論文の詳細を見る
Software model checking is typically applied to components of large systems. The assumption generation is the problem of finding the least restrictive environment in which the components satisfy a given safety property. There is an algorithm to compute the environment for properties given as a regular language. In this paper, we propose a general scheme for computing the assumption even for non-regular properties, and show the uniqueness of the least restrictive assumption for any class of languages. In general, dealing with non-regular languages may fall into undecidability of problems. We also show a method to compute assumptions based on visibly pushdown automata and their finite-state abstractions.
- 電子情報通信学会の論文
- 2009-02-01
著者
-
HIRAISHI Kunihiko
School of Information Science, Japan Advanced Institute of Science and Technology
-
Kucera Petr
Faculty Of Mathematics And Physics Charles University
-
Hiraishi Kunihiko
School Of Information Science Japan Advanced Institute Of Science And
関連論文
- Inkdot versus Pebble over Two-Dimensional Languages
- Application of DES Theory to Verification of Software Components
- Reduced State Space Generation of Concurrent Systems Using Weak Persistency (Special Section on Net Theory and Its Applications)
- Performance Evaluation of Workflows Using Continuous Petri Nets with Interval Firing Speeds
- A Heuristic Algorithm for One-Machine Just-In-Time Scheduling Problem with Periodic Time Slots
- Scheduling of parallel identical machines to maximize the weighted number
- On Symbolic Model Checking in Petri Nets
- The completeness of linear logic for petri net models
- The completeness of linear logic with modal operator for Petri net models
- Construction of Rule Base for the Control of Discrete Event Dynamic
- A Polynomial Time Algorithm for a Just-In-Time Scheduling Problem with Periodic Time Slots
- AS-3-3 A Workflow-based Change Support Model for Collaborative Software Development
- KCLP-HS: a rapid prototyping tool for implementing algorithms on hybrid systems
- A Petri-Net-Based Model for the Mathematical Analysis of Multi-Agent Systems
- Application of Interval Methods to Sampled-Data Control of Uncertain Piecewise Affine Systems