Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
9657453 | Science of Computer Programming | 2005 | 19 Pages |
Abstract
In this work we introduce a new formal model for software components supporting behavioral interpretability based on temporal logic, Petri nets, model checking, and an assume-guarantee strategy to specify and reason about the composition of concurrent component systems. The formal specification and verification strategies, methods, and techniques presented in this work contribute to the development of more dependable component-based software systems, in a modular way. An approach based on two complementary formalisms, Hierarchical Colored Petri Nets (HCPN) and temporal logic, is introduced. HCPN are used to visualize the structure and model the behavior of software architectures and components, and temporal logic is used to specify the required properties of software architectures and component interfaces.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Leandro Dias da Silva, Angelo Perkusich,