Analyses are central to the engineering of cyber-physical systems: they support design decisions, ensure safety, and provide evidence for certification. Yet re-executing analyses as models evolve is costly, and it is often unclear which prior results remain valid after a change. Existing formalisations in model-driven development (MDD) address models and their consistency, but leave the analyses themselves and their interdependencies underexplored. This limitation prevents systematic reuse of analysis results and inhibits techniques such as analysis slicing or incremental reanalysis, both of which require precise reasoning about analyses and their dependencies. We formalise analyses as first-class citizens alongside models. We define a formal model that characterises inputs, outputs, preconditions, properties, and trigger conditions, and we capture interdependencies through an analysis dependency graph. We further present an incremental recertification procedure that computes an analysis slice, identifying those analyses that must be re-executed to preserve global certification goals after model changes. We prove a core analysis theorem, establishing the soundness and completeness of this procedure. We enable analysis-aware consistency management across heterogeneous models. Two illustrative examples, in software development and ISO 26262-compliant automotive safety assurance, demonstrate the applicability of the approach and show analytically that selective re-execution can substantially reduce reanalysis effort. This paper contributes to the foundational theory of MDD by establishing a formal semantic framework for analyses and their interdependencies, laying the groundwork for future tool support and empirical validation.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Analyses as First-Class Citizens in Model-Driven Development

  • Tianhai Liu,
  • Shmuel Tyszberowicz,
  • Bernhard Beckert

摘要

Analyses are central to the engineering of cyber-physical systems: they support design decisions, ensure safety, and provide evidence for certification. Yet re-executing analyses as models evolve is costly, and it is often unclear which prior results remain valid after a change. Existing formalisations in model-driven development (MDD) address models and their consistency, but leave the analyses themselves and their interdependencies underexplored. This limitation prevents systematic reuse of analysis results and inhibits techniques such as analysis slicing or incremental reanalysis, both of which require precise reasoning about analyses and their dependencies. We formalise analyses as first-class citizens alongside models. We define a formal model that characterises inputs, outputs, preconditions, properties, and trigger conditions, and we capture interdependencies through an analysis dependency graph. We further present an incremental recertification procedure that computes an analysis slice, identifying those analyses that must be re-executed to preserve global certification goals after model changes. We prove a core analysis theorem, establishing the soundness and completeness of this procedure. We enable analysis-aware consistency management across heterogeneous models. Two illustrative examples, in software development and ISO 26262-compliant automotive safety assurance, demonstrate the applicability of the approach and show analytically that selective re-execution can substantially reduce reanalysis effort. This paper contributes to the foundational theory of MDD by establishing a formal semantic framework for analyses and their interdependencies, laying the groundwork for future tool support and empirical validation.