Model-Driven Architecture (MDA) presents a set of layered models to separate design concerns from platform concerns. The model executability for each model element is still challenging although MDA is currently able to cope with most syntactic and transformation definition issues. Moreover, the importance of rigorous specification and verification of the system is increasing, as the embedded software is more widely used for systems closely related to our life. Thus, this paper suggests behavior modeling views characterizing Platform-Independent Model (PIM) and Platform-Specific Model (PSM) behaviors and formal and verifiable models for them. In this, the PIM behavior is given from the view of the functionality of the software in Statecharts, whereas the PSM behavior is modeled from the view of a timed and resource-constrained behavior in TRoS, an extension of Statecharts in respect of time and resource constraints. Moreover, we provide an efficient way where PIM in Statecharts is transformed into PSM in TRoS. Using our approach, PIM and PSM behavior are captured in formal semantics for rigorous analysis in terms of system behavior, and the PSM behavior in TRoS is effectively and consistently obtained from the PIM behavior in Statecharts. We present a case study, in which safety-critical software for a railway control system is developed to show the feasibility of our approach.
模型驱动架构(MDA)提出了一组分层模型,以将设计关注点与平台关注点分离。尽管MDA目前能够处理大多数语法和转换定义问题,但每个模型元素的模型可执行性仍然具有挑战性。此外,随着嵌入式软件更广泛地应用于与我们生活密切相关的系统,对系统进行严格规范和验证的重要性日益增加。因此,本文提出了表征平台无关模型(PIM)和平台特定模型(PSM)行为的行为建模视图以及针对它们的形式化且可验证的模型。在此,PIM行为是从状态图中软件的功能角度给出的,而PSM行为是从TRoS(一种在时间和资源约束方面对状态图的扩展)中具有时间和资源约束的行为角度进行建模的。此外,我们提供了一种将状态图中的PIM转换为TRoS中的PSM的有效方法。使用我们的方法,PIM和PSM行为在形式语义中被捕获,以便从系统行为的角度进行严格分析,并且TRoS中的PSM行为能够从状态图中的PIM行为有效且一致地获得。我们展示了一个案例研究,其中开发了用于铁路控制系统的安全关键软件,以证明我们方法的可行性。