Logo des Repositoriums

Auflistung nach Autor:in "Kanig, Johannes"

1 - 2 von 2
  • Zeitschriftenartikel
    Hi-Lite - Verification by Contract
    (Softwaretechnik-Trends Band 31, Heft 3, 2011) Kanig, Johannes; Guitton, Jérôme; Moy, Yannick
    Formal methods and testing are often considered as disjoint technologies. The Hi-Lite project wants to show that both are actually complementary. The central concept are subprogram contracts, part of the upcoming Ada 2012 standard. A contract, which consists of pre- and postcondition, describes the specification of a subprogram, in the same syntax as Ada expressions. These contracts can be seen either as additional assertions in the case of testing, or they can be used to prove the correctness of the subprogram, using modern proof technology such as SMT solvers. This mechanism allows an easy adoption of modern formal methods, on a per-function basis. Hi-Lite fits in well with the upcoming DO-178C avionics safety standard, a revision to DO-178B, which, among other things, accounts for technologies such as formal methods. A contract is additional information a programmer has to write, and errors are possible. Another focus of the Hi-Lite project is to help the programmer write meaningful and complete contracts. Current proposals include the detection of runtime errors contained in contracts, meaningless or too strong contracts, incomplete contracts that do not mention modified variables and code that does not contribute to the contract. The goal of project Hi-Lite is to produce a verification toolchain combining formal methods and testing, integrated with the usual project structure in the two IDEs developed by AdaCore.
  • Konferenzbeitrag
    Integration von Formaler Verifikation und Test
    (Automotive - Safety & Security 2012, 2012) Comar, Cyrille; Kanig, Johannes; Moy, Yannick
    Üblicherweise nehmen die Verifizierungsaufgaben, die von den branchenspezifischen Standards gefordert werden, einen großen Teil der Entwicklungskosten von kritischen Systemen ein. Diese Tendenz wird noch verstärkt, da die Entwicklung und Pflege einer großen Menge von funktionalen und Robustheitstests, für immer komplexer werdende Anwendungen, nötig ist. Die formale Verifikation ist ein Weg, diese Kosten zu reduzieren, und bietet dabei gleichzeitig mehr Garantien. Neuere Standards, wie der Avionik-Standard DO- 178C, erlauben die Verifizierung von Software durch formale Methoden. Im Hi-Lite Projekt streben wir die Integration von Test und formaler Verifikation für C- und Ada-Entwicklungen an. In diesem Artikel beschreiben wir die Bedingungen, unter welchen eine solche Integration die gleichen Garantien geben kann wie eine Verifikation ausschließlich durch Test. Wir beschreiben ebenfalls die Vorund Nachteile einer solchen Methode, mithilfe einer Datenbankapplikation als Fallstudie.