Research output

Conference Paper (in Formal Publication) ()

Omnibus: a clean language and supporting tool for integrating different assertion-based verification techniques

Citation
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.

Abstract
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.

StatusPublished
EditorButler M, Jones C, Romanovsky A, Troubitsyna E
AuthorsWilson Thomas, Maharaj Savi, Clark Robert
Title of seriesTechnical Report Series
Number in seriesCS-TR-915
Publication date2005
Date of public distribution07/2005
URLhttp://rodin.cs.ncl.ac.uk/REFT.htm
PublisherUniversity of Newcastle upon Tyne
Place of publicationNewcastle upon Tyne
LanguageEnglish
© University of Stirling FK9 4LA Scotland UK • Telephone +44 1786 473171 • Scottish Charity No SC011159
My Portal