Information Technology Reference
In-Depth Information
3. a method for using these tools to construct and verify a family of similar
control systems.
For each control system to be generated, the user makes a description of the
application-specific parameters in the domain-specific language and checks the
description by means of the syntax and static semantics checker. Then from this
description the generators produce models of the control system and its physical
environment, together with the safety requirements which are automatically ver-
ified using the bounded model checker in combination with an inductive proof
strategy. Finally - since the formal controller model can be directly compiled -
object code is generated by a conventional compiler, and it is checked by the ob-
ject code verifier that the object code is behaviourally equivalent to the control
system model. In this way it is ensured that the safety properties established for
the control system model also hold for the object code.
The development of the framework was formalised by using the RAISE for-
mal method, thereby providing complete and precise specifications of the tools
as well as the domain-specific language. This provides a sound basis for tool
implementation and allows for formal verification of algorithms.
References
1. Accellera. Property Specification Language Version 1.1 (2004)
2. Badban, B., Franzle, M., Peleska, J., Teige, T.: Test automation for hybrid systems.
In: Proceedings of the Third International Workshop on SOFTWARE QUALITY
ASSURANCE (SOQUA 2006), Portland Oregon, USA, November 2006 (2006)
3. Berkenkotter, K.: OCL-based validation of a railway domain profile. In: OCLApps
2006 - OCL for (Meta-)Models in Multiple Application Domains, October 2006
(2006)
4. Bjørner, D.: Domain Engineering: A ”Radical Innovation” for Software and Sys-
tems Engineering? A Biased Account. In: Dershowitz, N. (ed.) The Zohar Manna
Intl.Symp. on Verification: Theory & Practice, Heidelberg, Germany, Springer,
Heidelberg (2003)
5. Bjørner, D.: New Results and Current Trends in Formal Techniques for the Devel-
opment of Software for Transportation Systems. In: Proceedings of the Symposium
on Formal Methods for Railway Operation and Control Systems (FORMS'2003),,
Budapest/Hungary, May 15-16 2003, L'Harmattan Hongrie (2003)
6. Bjørner, D.: Railways systems: Towards a domain theory. Technical report, Infor-
matics and Mathematical Modelling, Technical University of Denmark, Building
322, Richard Petersens Plads, DK-2800 Kgs.Lyngby, Denmark (2003)
7. Bjørner, D.: Software Engineering. Abstraction and Modelling. Texts in Theoretical
Computer Science, vol. 1, Springer, Heidelberg (2006)
8. Bjørner, D.: Software Engineering. Specification of Systems and Languages. Texts
in Theoretical Computer Science, vol. 2, Springer, Heidelberg (2006)
9. Bjørner, D.: Software Engineering. Domains, Requirements and Software Design.
Texts in Theoretical Computer Science, vol. 3, Springer, Heidelberg (2006)
10. Bjørner, D.: The Role of Domain Engineering in Software Development. Invited
keynote paper and talk: IPSJ/SIGSE Software Engineering Symposium 2006,
Tokyo (October 2006)
Search WWH ::




Custom Search