CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Integration of Informal and Formal Development of Object-Oriented Safety-Critical Software: A Case Study with the KeY System

R. Bubel ; Reiner Hähnle (Institutionen för datavetenskap)
Electronic Notes in Theoretical Computer Science. Eight International Workshop on Formal Methods for Industrial Critical Systems (FMICS'03), Röros, 5-7 June 2003 (1571-0661). Vol. 80 (2003), p. 3-25.
[Konferensbidrag, refereegranskat]

The KeY system allows integrated informal and formal development of objectoriented Java software. In this paper we report on a major industrial case study involving safety-critical software for computation of a particular kind of railway time table used by train drivers. Our case study includes formal specification of requirements on the analysis and the implementation level. Particular emphasis in our research is put on the challenge of how authoring and maintenance of formal specifications can be made easier. We demonstrate that the technique of specification patterns implemented in KeY for the language OCL yields significant improvements.



Denna post skapades 2013-02-28.
CPL Pubid: 174227

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för datavetenskap (2002-2004)

Ämnesområden

Data- och informationsvetenskap

Chalmers infrastruktur