Loading...
Please wait, while we are loading the content...
Similar Documents
Software Component Verification : On Translating Behavior Protocols to Promela ∗ Technical Report
| Content Provider | Semantic Scholar |
|---|---|
| Author | Kofron, Jan |
| Copyright Year | 2006 |
| Abstract | Using software components is a modern approach for building extensible and reliable applications. To ensure high dependability, a component application should undergo verification, e.g. model checking, to prove it has certain properties. The implementation of an application is usually too complex to be verified at a formal level; therefore, a model being an abstraction of the implementation is to be used. Behavior protocols [10] are a platform for modeling of software component behavior. In this paper, we propose a method for translation behavior protocols to Promela [7], which is consequently used as the input for the Spin model checker [7]. Having the Promela code describing the component behavior, one can efficiently check for the behavior compatibility and LTL (Linear Temporal Logic) properties of cooperating software components. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://d3s.mff.cuni.cz/publications/download/Kofron-bp2prom-tr.pdf |
| Alternate Webpage(s) | http://d3s.mff.cuni.cz/publications/Kofron-bp2prom-tr.pdf |
| Alternate Webpage(s) | http://dsrg.mff.cuni.cz/publications/Kofron-bp2prom-tr.pdf |
| Alternate Webpage(s) | http://nenya.ms.mff.cuni.cz/publications/Kofron-bp2prom-tr.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
