Gerichtete und parallele Validierung von abstrakten Spezifikationen

抽象规范的定向和并行验证

• 批准号: 53141881
• 负责人: Professor Dr. Michael Leuschel
• 金额: --
• 依托单位: Arbeitsgruppe Softwaretechnik und Programmiersprachen
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2007
• 资助国家: 德国
• 起止时间: 2006-12-31 至 2013-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/53141881?language=en
• 关键词: Gerichtete; und; parallele; Validierung; von

Formale Methoden haben das Ziel fehlerfreie Software zu produzieren. Die B-Methode ist eine formale Methode die erfolgreich in mehreren Industrie-Projekten angewandt wurde. Mit steigender Komplexität industrieller Anforderungen an Softwaresysteme wird auch das Erstellen korrekter Spezifikationen schwieriger. Jeder Fehler in der Ausgangsspezifikation tritt auch in der resultierenden Software auf, daher stellt die Korrektheit der Spezifikation einen kritischen Punkt dar. Das Hauptziel dieses Forschungsprojektes ist es, Methoden und Werkzeuge zu entwickeln, mit denen aus Industrieprojekten stammende, komplexe, formale B-Spezifikationen validiert werden können. Eine besondere Herausforderung dabei ist die hohe Ausdruckskraft der B Spezifikationssprache. Wir glauben, dass gerade in dieser hohen Abstraktionsebene ein großes Potential für intelligente Validierungstechniken steckt. In diesem Projekt wollen wir folgende zwei Techniken entwickeln: gerichtetes Modelchecking von B, um Fehlerzustände in großen Zustandsräumen anhand von Heuristiken zu finden, sowie paralleles Modelchecking, zur Verteilung des Rechenaufwandes. Beide Techniken sollen durch genetische Optimierung und statische Analyse unterstützt werden.

形式上的方法是生产各种各样的免费软件。B-方法是一种在许多工业项目中进行试验的正式方法。工业上的复杂软件系统也会被认为是一个更复杂的系统。Jeder Fehler在Ausgangsspezifikation中也在结果软件中使用，因此Spezifikation的错误是一个关键点。这些主要的研究项目是一种新的方法和工具，它包括工业项目、复杂的项目、正式的B-Spezifikationen validiert韦尔登项目。一个最好的纪念品是B特殊包装的最高水平。我们希望，在这个高度抽象化的过程中，有一个巨大的潜力可以用于智能验证技术。在这个项目中，我们将进行两项技术研究：B的模型检验，在大的Zustandsräumen中的Fehlerzustände和Heuristiken zu finden，sowie paralleles Modelchecking，zur Verteilung des Rechenaufwandes。Beide Techniken sollen durch genetische optimierung und statistische Analyse unterstützt韦尔登.

项目成果

Inferring physical units in formal models

推断正式模型中的物理单位

• DOI: 10.1007/s10270-015-0458-0
• 发表时间: 2017
• 期刊: Software & Systems Modeling
• 影响因子: 2
• 作者: Sebastian Krings;Michael Leuschel
• 通讯作者: Michael Leuschel

Optimising the ProB model checker for B using partial order reduction

使用偏序约简优化 B 的 ProB 模型检查器

• DOI: 10.1007/s00165-015-0351-1
• 发表时间: 2014
• 期刊: Formal Aspects of Computing
• 影响因子: 1
• 作者: Ivaylo Dobrikov;Michael Leuschel
• 通讯作者: Michael Leuschel

Translating B to TLA + for Validation with TLC

将 B 转换为 TLA 以使用 TLC 进行验证

• DOI: 10.1007/978-3-662-43652-3_4
• 发表时间: 2014
• 作者: Dominik Hansen;Michael Leuschel
• 通讯作者: Michael Leuschel