| Autor: | Bernd J. Krämer, Norbert Völker, Reiner Lichtenecker, Hans-Friedrich Kötter |
|---|---|
| Rok vydání: | 1998 |
| Předmět: |
Model checking
Object-oriented programming Computer science business.industry Programming language Software development Specification language Interface description language computer.software_genre Common Object Request Broker Architecture TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Formal specification General Earth and Planetary Sciences business Implementation computer |
| Zdroj: | Journal of Systems Integration. 8:143-158 |
| ISSN: | 0925-4676 |
| DOI: | 10.1023/a:1008226622237 |
| Popis: | This article describes an approach to the development of highly reliable and reusable CORBA applications. Interface description language (IDL) specifications are extended with LOTOS specifications of the functional and dynamic behavior of the interface operations. These extended interface specifications are compiled into header files and stub code using standard CORBA mechanisms. The LOTOS part can be compiled into C-code yielding prototype implementations. An extensible set of LOTOS tools is used to test and prove critical properties of distributed applications. From the event-oriented LOTOS description, a state-oriented program in a CSP-like programming language is derived. This program can be analyzed using very efficient, BDD-based model checking verification tools. Furthermore, it serves as an ideal intermediate step between verified, high level, reusable LOTOS processes which solve typical distributed programming tasks and their implementation as CORBA objects in production programming languages. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink