Optimale Interprozeduale Analyse von Programmen mit dynamischer Thread-Erzeugung
Optimale Interprozeduale Analyse von Programmen mit dynamischer Thread-Erzeugung
批准号:
52609764
负责人:
Professor Dr. Markus Müller-Olm
金额:
$0.0万
依托单位:
依托单位国家:
德国
项目类别:
Research Grants
财政年份:
2007
资助国家:
德国
项目状态:
已结题
起止时间:
2006-12-31 至 2016-12-31
中文摘要
点击翻译按钮获取中文摘要
英文摘要
In der ersten Projektphase wurden Methoden entwickelt, um den Kontrofluss in nebenläufigen Programmen mit Synchronisationsprimitiven präzise zu analysieren. Dabei konzentrierten wir uns einerseits auf dynamische Pushdown-Netzwerke (DPNs) mit wohlgeschachtelten Locks oder Monitoren. Auf der anderen Seite untersuchten wir ein vereinfachtes Taskmodell, das dem Automobilstandard Osek zu Grunde liegt, bei dem unterschiedliche Tasks mit Hilfe von Ressourcen und Prioritäten synchronisiert werden. Darauf aufbauend sollen nun in dem Nachfolgeprojekt für diese Programmiermodelle Analyseframeworks entwickelt werden, die es erlauben, weiterreichende Programmeigenschaften statisch zu ermitteln. Insbesondere sollen sowohl für das Osek-Modell als auch für DPNs Wertanalysen für Programme mit globalen Variablen entwickelt werden. Zur Steigerung der Präzision sollen diese Analysen Synchronisationsprimitive mitberücksichtigen. Neben den schon in der ersten Projektphase betrachteten Synchronisationsprimitiven sollen zudem weitere Synchronisationskonzepte identifiziert werden, die exakt behandelt werden können.
期刊论文(10)
专著(0)
科研奖励(0)
会议论文
登录
查看更多内容
DOI:
10.1007/978-3-642-02658-4_39
发表时间:
2009-06
期刊:
影响因子:
--
作者:
[P. Lammich;M. Müller-Olm;A. Wenner]
通讯作者:
P. Lammich;M. Müller-Olm;A. Wenner
Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs
优先级调度程序中值相关同步的精确分析
DOI:
10.1007/978-3-642-54013-4_2
发表时间:
2014
期刊:
影响因子:
--
作者:
[M. Schwarz, H. Seidl, V. Vojdani, K. Apinis]
通讯作者:
K. Apinis
Iterable Forward Reachability Analysis of Monitor-DPNs
Monitor-DPN 的可迭代前向可达性分析
DOI:
10.4204/eptcs.129.24
发表时间:
2013
期刊:
影响因子:
--
作者:
[B. Nordhoff, M. Müller-Olm, P. Lammich]
通讯作者:
P. Lammich
DOI:
10.1007/978-3-642-11957-6_31
发表时间:
2010-03
期刊:
影响因子:
--
作者:
[A. Wenner]
通讯作者:
A. Wenner
Normalization of Linear Horn Clauses
线性 Horn 子句的规范化
DOI:
10.1007/978-3-642-19829-8_16
发表时间:
2010
期刊:
影响因子:
--
作者:
[T. M. Gawlitza, H. Seidl, K. N. Verma]
通讯作者:
K. N. Verma
共 10 条
Information Flow Control for Mobile Components Based on Precise Analysis for Parallel Programs
-
批准号:183297858
-
项目类别:Priority Programmes
-
资助金额:$0.0万
-
财政年份:2010
-
负责人:Professor Dr. Markus Müller-Olm
-
依托单位:
Model Checking of Navigation Logics (MoNaLog)
-
批准号:436811065
-
项目类别:Research Grants
-
资助金额:$0.0万
-
财政年份:--
-
负责人:Professor Dr. Markus Müller-Olm
-
依托单位: