Interfacing Ada with verification languages
| Autor: | David Andrews, Glenn H. MacEwen, David Leeson |
|---|---|
| Rok vydání: | 1994 |
| Předmět: |
General-purpose programming language
Functional verification Programming language Computer science business.industry Software development computer.software_genre Software construction General Earth and Planetary Sciences Verification Software verification and validation Software system business computer Software verification General Environmental Science |
| Zdroj: | Proceedings of the second international symposium on Environments and tools for Ada - SETA2. |
| ISSN: | 0736-721X |
| Popis: | Ada is a general purpose programming language suitable for use in large applications and/or embedded real-time applications. However, its use in verification, i.e., the mathematical proof that a program's implementation is consistent with its specification, poses significant problems.One potential solution to this problem is to allow the integration of Ada software with other software that has been verified. The implications of integrating Ada with a verification language extend well beyond the technical challenge of developing language-heterogenous software systems. Not only must one implement a way to allow this integration, but one must do it in such a way as to not invalidate the underlying assumptions of the verification effort.The question as to whether it makes sense to integrate trusted (verified) and untrusted (Ada) software is addressed. The conclusion is that with proper decomposition, and the understanding that the goal is to verify specific properties and not entire programs, it is feasible to do this and still maintain the validity of the verification effort.Several integration approaches are presented. The most promising, separate processes communicating via remote procedure calls, is studied in more detail and a high level design for an implementation is described. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|