Formal Verification of Object-Oriented Graph Grammars Specifications
| Autor: | Luciana Foss, Ana Paula Lüdtke Ferreira, Leila Ribeiro |
|---|---|
| Rok vydání: | 2007 |
| Předmět: |
Model checking
Object-oriented programming Theoretical computer science Correctness General Computer Science Computer science business.industry Programming language Concurrency object-oriented programming computer.software_genre model checking Graph grammars Theoretical Computer Science Software Promela Graph (abstract data type) SPIN model checker business Formal verification computer Computer Science(all) computer.programming_language |
| Zdroj: | Electronic Notes in Theoretical Computer Science. 175:101-114 |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2007.04.020 |
| Popis: | Concurrent object-oriented systems are ubiquitous due to the importance of networks and the current demands for modular, reusable, and easy to develop software. However, checking the correctness of such systems is a hard task, mainly due to concurrency and inheritance aspects. In this paper we present an approach to the verification of concurrent object-oriented systems. We use graph grammars equipped with object oriented features (including inheritance and polymorphism) as the specification formalism, and define a translation from such specifications to Promela, the input language of the SPIN model checker. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect