Unvollständige automatische Verifikation von Software-Designmodellen für nebenläufige objektorientierte eingebettete Echtzeitsysteme basierend auf dem Paradigma der erweiterten kommunizierenden Zustandsautomaten.

基于扩展通信状态机范式的并发面向对象嵌入式实时系统软件设计模型的不完全自动验证。

• 批准号: 5364050
• 负责人: Professor Dr. Stefan Leue
• 金额: --
• 依托单位: Arbeitsgruppe Software und Systems Engineering
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2002
• 资助国家: 德国
• 起止时间: 2001-12-31 至 2009-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/5364050?language=en
• 关键词: Unvollst; ndige; automatische; Verifikation; von

Das Ziel des Projekts ist es, automatische Verifikationstechniken auf hierarchische objektorientierte Modelle (wie z.B. UML-RT) anwendbar zu machen. Da diese Modelle bei praktischen Anwendungen häufig sehr große oder unendliche Zustandsräume besitzen, versagen klassische automatische Model Checking Algorithmen bei ihrer Analyse. In diesem Projekt sollen erstens verschiedene unvollständige Model Checking Algorithmen und andere Techniken (z.B. Akzeleration) auf ihre Anwendbarkeit auf UML-RT Modelle untersucht werden. Zweitens soll eine zentrale Schnittstelle geschaffen werden, die ein gegebenes Modell Analysiert, die geeignetste Verifikationsmethode auswählt und die Ergenisse interpretiert und für den Benutzer darstellt.

项目的Ziel是一种基于层次对象模型的自动验证技术（如Z.B. UML-RT）anwendbar zu machen.在实际应用中，该模型的规模很大，但也有很大的局限性，因此在分析中采用经典的自动模型检验方法。在这个项目中，sollen将使用模型检验方法和技术（z.B. Akzeleration）在UML-RT模型的基础上进行了韦尔登。两种方法都需要一个中间的Schnittstelle geschaffen韦尔登，一个通用的分析模型，通用的验证方法，以及对Benutzer darstelt的解释。

项目成果

An AsmL Semantics for Dynamic Structures and Run Time Schedulability in UML-RT

UML-RT 中动态结构和运行时可调度性的 AsmL 语义

• DOI: 10.1007/978-3-540-69824-1_14
• 发表时间: 2008
• 作者: Stefan Leue;Alin Stefanescu;Wei Wei
• 通讯作者: Wei Wei

Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs

• DOI: 10.29007/c7v2
• 发表时间: 2010
• 作者: M. Kuntz;S. Leue;Christoph Scheben

Integer Linear Programming-Based Property Checking for Asynchronous Reactive Systems

• DOI: 10.1109/tse.2011.1
• 发表时间: 2013-02
• 期刊: IEEE Transactions on Software Engineering
• 影响因子: 7.4
• 作者: S. Leue;Wei Wei-Wei

Counterexample Explanation by Anomaly Detection

• DOI: 10.1007/978-3-642-31759-0_5
• 发表时间: 2012-07
• 作者: S. Leue;Mitra Tabaei Befrouei