Conference Paper (in Formal Publication) ()
Wilson T, Maharaj S & Clark R (2005) Omnibus: a clean language and supporting tool for integrating different assertion-based verification techniques In: Butler M, Jones C, Romanovsky A, Troubitsyna E (ed.) Proceedings of the Workshop on Rigorous Engineering of Fault-Tolerant Systems (REFT 2005), Newcastle upon Tyne: University of Newcastle upon Tyne. Workshop on Rigorous Engineering of Fault-Tolerant Systems (REFT 2005), 19.7.2005 - 19.7.2005, Newcastle, pp. 43-52.
Omnibus is a new system for the development of reliable Object- Oriented software. It includes a clean language that is superficially similar to Java but removes aspects that particularly complicate verification. Integrated support is provided for run-time assertion checking, extended static checking and full formal verification. The language is supported by a prototype IDE with a type checker, Java code generator, HTML documentation generator and a range of verifiers. This paper presents the case for Omnibus, gives an overview of the language and tools and discusses its relationship to dependable systems development.
|Editor||Butler M, Jones C, Romanovsky A, Troubitsyna E|
|Authors||Wilson Thomas, Maharaj Savi, Clark Robert|
|Title of series||Technical Report Series|
|Number in series||CS-TR-915|
|Date of public distribution||07/2005|
|Publisher||University of Newcastle upon Tyne|
|Place of publication||Newcastle upon Tyne|