Validation of Stochastic Systems 2

随机系统的验证 2

基本信息

项目摘要

Embedded systems are computer systems that control more and more things in our lives - from elevators, to cars, to aircraft. There is a lot of software that runs on these systems and very often these systems have to operate in safety critical situations, like the software that runs the fuel injection of a car or controls the airbags. More and more, embedded systems consist of large networks of interacting computing devices, which further complicates design and analysis. It is of utmost importance that there are no errors in safety critical systems. Our research focuses on methods to find and prevent such errors. More specifically, the VOSS2 project aims at the integration of modeling and computer-aided verification techniques for the analysis of complex systems with stochastic behavior. Rather than proving that systems will always behave correct, we aim at establishing properties like "the probability that an airbag will be deployed inadvertently during its operational life is less than 10-9". Our goal is to adapt and extend some prominent techniques that have been successful for modeling and assessing qualitative characteristics of computer systems to a stochastic setting. Modeling techniques such as input-output (I/O) automata and process algebra, and verification techniques such as model checking will be thoroughly investigated. We plan to apply these techniques to model, analyze, and optimize systems described as Markov processes.
嵌入式系统是控制我们生活中越来越多事物的计算机系统 - 从电梯到汽车,再到飞机。这些系统上运行有很多软件,而且这些系统通常必须在安全关键情况下运行,例如运行汽车燃油喷射或控制安全气囊的软件。嵌入式系统越来越多地由交互计算设备的大型网络组成,这使得设计和分析变得更加复杂。最重要的是,安全关键系统中不存在错误。我们的研究重点是发现和防止此类错误的方法。更具体地说,VOSS2 项目旨在集成建模和计算机辅助验证技术,以分析具有随机行为的复杂系统。我们的目标不是证明系统始终表现正确,而是建立诸如“安全气囊在其使用寿命期间无意中展开的概率小于 10-9”之类的属性。我们的目标是将一些在随机环境中成功建模和评估计算机系统定性特征的突出技术进行调整和扩展。将彻底研究输入输出(I/O)自动机和过程代数等建模技术以及模型检查等验证技术。我们计划应用这些技术来建模、分析和优化被描述为马尔可夫过程的系统。

项目成果

期刊论文数量(0)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ monograph.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ patent.updateTime }}

Professorin Dr. Christel Baier其他文献

Professorin Dr. Christel Baier的其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

{{ truncateString('Professorin Dr. Christel Baier', 18)}}的其他基金

Temporal Logics and Probabilistic Model Checking for Weighted Structures
加权结构的时态逻辑和概率模型检查
  • 批准号:
    289295178
  • 财政年份:
    2016
  • 资助金额:
    --
  • 项目类别:
    Research Grants
Unambiguity, alternation and non-standard acceptance in automata-based probabilistic model checking
基于自动机的概率模型检查中的明确性、交替性和非标准接受
  • 批准号:
    313089026
  • 财政年份:
    2016
  • 资助金额:
    --
  • 项目类别:
    Research Grants
RigorOus dependability analysis using model ChecKing techniques for Stochastic systems (ROCKS)
使用随机系统模型检查技术 (ROCKS) 进行严格的可靠性分析
  • 批准号:
    133365105
  • 财政年份:
    2009
  • 资助金额:
    --
  • 项目类别:
    Research Grants
Verifikation quantitativer Eigenschaften eines Mikrokernbetriebssystems durch eine Kombination von probabilistischem Model Checking und interaktivem Theorembeweisen
通过概率模型检查和交互式定理证明相结合来验证微内核操作系统的定量特性
  • 批准号:
    147212833
  • 财政年份:
    2009
  • 资助金额:
    --
  • 项目类别:
    Research Grants
Synthesis and Analysis of Component Connectors (SYANCO)
元件连接器的综合与分析(SYANCO)
  • 批准号:
    19965642
  • 财政年份:
    2006
  • 资助金额:
    --
  • 项目类别:
    Research Grants
Reduktionsmethoden zur Verifikation omega-regulärer und temporallogischer Eigenschaften für kommunizierende probabilistische Prozesse
用于验证用于通信概率过程的欧米伽正则和时间逻辑属性的约简方法
  • 批准号:
    5438551
  • 财政年份:
    2004
  • 资助金额:
    --
  • 项目类别:
    Research Grants
Computerunterstützte Verifikation mit abstrakten Modellen
抽象模型的计算机辅助验证
  • 批准号:
    5344856
  • 财政年份:
    2001
  • 资助金额:
    --
  • 项目类别:
    Research Grants

相似国自然基金

弱耗散随机动力系统的平均原理
  • 批准号:
    12371188
  • 批准年份:
    2023
  • 资助金额:
    43.5 万元
  • 项目类别:
    面上项目
随机干扰作用下轮毂电机驱动电动汽车悬架系统有限时间稳定与容错控制
  • 批准号:
    62363013
  • 批准年份:
    2023
  • 资助金额:
    32 万元
  • 项目类别:
    地区科学基金项目
随机噪声下分数阶关联非线性系统的分散主动抗干扰控制
  • 批准号:
    62303397
  • 批准年份:
    2023
  • 资助金额:
    30 万元
  • 项目类别:
    青年科学基金项目
耦合系统在随机扰动下长时间动力学行为的研究
  • 批准号:
    12371177
  • 批准年份:
    2023
  • 资助金额:
    43.5 万元
  • 项目类别:
    面上项目
非瞬时脉冲条件下分数阶随机系统的稳定性及其相关研究
  • 批准号:
    12361035
  • 批准年份:
    2023
  • 资助金额:
    27 万元
  • 项目类别:
    地区科学基金项目

相似海外基金

Resolving Spatiotemporal Determinants of Cell Specification in Corticogenesis with Latent Space Methods
用潜在空间方法解决皮质生成中细胞规格的时空决定因素
  • 批准号:
    10378061
  • 财政年份:
    2021
  • 资助金额:
    --
  • 项目类别:
Resolving Spatiotemporal Determinants of Cell Specification in Corticogenesis with Latent Space Methods
用潜在空间方法解决皮质生成中细胞规格的时空决定因素
  • 批准号:
    10703714
  • 财政年份:
    2021
  • 资助金额:
    --
  • 项目类别:
Resolving Spatiotemporal Determinants of Cell Specification in Corticogenesis with Latent Space Methods
用潜在空间方法解决皮质生成中细胞规格的时空决定因素
  • 批准号:
    10188106
  • 财政年份:
    2021
  • 资助金额:
    --
  • 项目类别:
Resolving Spatiotemporal Determinants of Cell Specification in Corticogenesis with Latent Space Methods
用潜在空间方法解决皮质生成中细胞规格的时空决定因素
  • 批准号:
    10703714
  • 财政年份:
    2021
  • 资助金额:
    --
  • 项目类别:
Stochastic tuning: a novel regulatory mechanism for cellular adaptation
随机调谐:细胞适应的新型调节机制
  • 批准号:
    10668425
  • 财政年份:
    2020
  • 资助金额:
    --
  • 项目类别:
{{ showInfoDetail.title }}

作者:{{ showInfoDetail.author }}

知道了