一种基于形式化规约生成软件体系结构模型的方法

使用LOTOS描述实时系统需求规约,通过建立LOTOS规约到UML-RT模型的模型转换,提出一种基于形式化规约生成软件体系结构模型的方法。最后,通过一个实例来说明如何将该方法应用于实时软件建模。利用这种方法建立的UML-RT模型,能够从整体上提高实时系统软件体系结构设计的可信性。     

一种基于代数语义的软件体系结构求精方法

软件体系结构是引导需求到实现的桥梁,目前在软件体系结构建模方法中主要分为形式化和非形式化两种。针对大型分布式系统的体系结构采用Petri网进行建模,兼顾了可视化操作和形式化的准确性,同时利用细化求精操作建立体系结构的层次模型,有效解决了状态空间爆炸问题。此外,在求精过程中为了保证用于下层求精的子网能准确表达上层行为规约,引入了进程代数来刻画Petri网的行为语义。最后,给出了进程项构造子网的算法及案例研究,并通过开源工具验证上述内容的正确性。     

基于扩展Petri网的系统建模及形式化验证方法*

嵌入式实时系统对时间约束性、安全性和可靠性具有非常高的要求,但是传统的建模和形式化验证方法难以满足对系统的实时性和安全性的模拟和验证需求。通过对有色Petri网的时间属性进行扩展,提出了实时有色Petri网模型,能够对系统的时间属性进行模拟和评估;参考实时有色Petri网模型到时间自动机的语义转换规则对模型进行转换,可以利用时间计算树逻辑对系统的实时性、安全性和可靠性进行形式化验证。以列车通信网络控制器的双线冗余控制模块的建模和形式化验证为例,证明了该方法的有效性。     

UML模型到COOZ规约的形式化转换

为UML建模元素提供坚实的形式化语义基础是目前的研究热点之一,在这方面也有了不少探索。文章在过去的研究的基础上,给出了UML模型到COOZ规约的一种系统的转化方法。将UML模型转换到COOZ规约后,UML模型的推理验证就可以通过相应COOZ规约的推理验证实现。该方法不但为UML提供了精确的形式化语义基础,而且,提供了一种UML模型推理的合理的机制。     

UML-RT在实时系统中的应用研究

采用UML-RT为实时应用的结构和行为建模的基本概念及策略,给出了实时系统分析和设计的方法;并以一个实时系统的结构模型和行为模型的实现为例,说明了利用UML-RT进行实时系统建模的具体过程.     

构件式体系结构模型映射的形式化语义

语义一致性是模型驱动开发中模型转换正确性的一个重要标准,但目前模型转换中语义特性保持的定义、描述和验证仍是一个尚未解决的难题.基于软件体系结构,利用范畴理论和代数规范形式化描述体系结构模型及其间的映射关系,使之具有精确的语义.体系结构模型的形式化语义用类型范畴图表来表示,态射合成被用来追踪构件模型之间的关联和映射,不同层次模型间的映射关系用态射和函子来形式化描述.以此为基础,进一步分析了模型转换应保持的语义特性.范畴理论支持图形化建模,可以使模型中的构件关系以及结构特征可视化,有利于对模型转换的理解和追踪.应用研究表明,该描述框架很好地把握了模型驱动开发的实质、过程和要求,为模型转换和模型驱动开发提供了新的认知、设计和语义计算的指导架构.     

基于STeC-Stateflow转换系统的实时系统仿真与验证方法

物联网以及信息物理融合系统对形式化建模提出了新的挑战, 引入了实时系统规范语言STeC, 为刻画实时系统的时空一致性提供了规范语言。针对STeC语言建立STeC至Stateflow自动转换系统, 提出一种基于STeC至Stateflow转换的仿真及验证方法, 该方法使用STeC语言对实时系统进行形式化建模, 再建立实时监控的Simulink仿真模型, 并使用Checkmate对系统进行安全性验证。通过对京沪高铁运行的实例研究, 表明该方法对高铁运行系统实时仿真的有效性, 并能够验证高铁运行系统的安全性。     

基于CSP的OWL-S语义分析与建模

为了实现OWL-S过程模型正确性的自动化验证,提出了基于进程代数CSP的OWL-S过程模型的语义建模方法,建立了CSP的形式化语义模型,并利用该模型为OWL-S过程定义了形式化语义。最后以机票预订为例说明了采用CSP模型为OWL-S过程添加形式化语义的完整流程。由于该方法具备良好的数学基础,所以可以基于该方法开发出自动化验证OWL-S过程模型的工具,提高系统的安全性。     

面向自然语言需求的验证性质生成方法

安全关键系统和软件的安全性、可靠性需要形式化验证来保障,使用形式化验证的前提是从自然语言需求文本中提取相关验证性质并将其转化为形式化规约,这已成为当前形式化验证领域研究的热点和难点.当前的形式化规约提取工作大多针对英文需求,较少针对中文自然语言需求.此外,由于AADL具有强大的表达能力和完善的验证机制,已成为航空航天领域的主要建模语言之一,而现有的工作较少考虑如何从需求中提取AADL模型的验证性质.为了解决上述问题,本文提出一种面向自然语言需求的AADL模型验证性质自动生成方法,从自然语言需求中提取验证的相关性质,并将其转化为AADL模型验证工具AGREE可识别的形式化规约.首先,定义了模式定义语言(Contract Pattern Language, CPL),将需求划分为不同模式,并给出由固定句型和占位符组成的需求模板;其次,通过自然语言处理技术解析需求文本,获取替换需求模板中占位符的原子命题,以便生成完整的形式化规约;最后,设计并实现了相关工具,并将其用于工业界实际案例来说明该方法的可用性和有效性.     

基于设计演算的形式化用例分析建模框架

提出一种形式化用例分析建模框架,引入类图、用例顺序图、用例状态图、功能规约函数和系统不变式从多个角度为需求建模.通过定义这些视图的形式化语义,为需求的各个方面定义了准确的形式化描述.利用该框架,可以从方法的交互行为规约和功能规约合成描述方法全部行为的全规约;也可以定义用例模型的性质,并通过设计演算中的证明来分析验证这些性质.作为应用,研究了检查用例模型一致性的规则.给出一个实例说明建模框架的可行性.     

An executable formal semantics for UML-RT

We propose a formal semantics for UML-RT, a UML profile for real-time and embedded systems. The formal semantics is given by mapping UML-RT models into a language called kiltera, a real-time extension of the \(\pi \)-calculus. Previous attempts to formalize the semantics of UML-RT have fallen short by considering only a very small subset of the language and providing fundamentally incomplete semantics based on incorrect assumptions, such as a one-to-one correspondence between “capsules” and threads. Our semantics is novel in several ways: (1) it deals with both state machine diagrams and capsule diagrams; (2) it deals with aspects of UML-RT that have not been formalized before, such as thread allocation, service provision points, and service access points; (3) it supports an action language; and (4) the translation has been implemented in the form of a transformation from UML-RT models created with IBM’s RSA-RTE tool, into kiltera code. To our knowledge, this is the most comprehensive formal semantics for UML-RT to date.     

Towards UML-based formal specifications of component-based real-time software

UML-RT is achieving increasing popularity as a modeling language for real-time applications. Unfortunately UML-RT is not formally well defined and it is not well suited for supporting the specification stage: e.g., it does not provide native constructs to represent time and non-determinism. UML+ is an extension of UML that is formally well defined and suitable for expressing the specifications of real-time systems (e.g., the properties of a UML+ model can be formally verified). However, UML+ does not support design and development. This article addresses the translation of UML+ into UML-RT, thus posing the basis for a development framework where UML+ and UML-RT are used together, in order to remove each other’s limitations. Specifications are written using UML+, they are automatically verified by means of formal methods, and are then converted – through a semi-automatic process – in an equivalent UML-RT model that becomes the starting point for the implementation.     

基于UML-RT的复杂嵌入式系统建模方法及其应用

分析了UML在实时系统设计中的优点和需要解决的主要问题,论述了基于UML RT的实时嵌入式系统设计方法,并且对其进行扩展以支持数据流计算模型的建模,最后以汽车巡航系统为例加以说明。     

基于Rebeca模型的硬件设计形式化验证

形式化验证是对传统验证方法的补充,是数字电路验证的一条有效途径,对于并发系统,行为建模是一种非常合适的建模方法;Rebeca是由Sirjani和Movaghar提出的一种基于行为的建模语言,支持形式化,一方面,Rebeca是一种类Java的语言,软件工程师很容易使用,另一方面,它是一种支持形式化验证及其相关理论的模型语言,可以为不精通于形式化方法的开发人员和研究人员提供方便的验证过程;在深入研究Rebeca的基础上,采用Rebeca对硬件设计进行建模,然后Modere形式化验证工具对AES密码芯片进行形式化验证。     

Generating tools from graph-based specifications

This paper describes an approach for generating graphical, structure-oriented software engineering tools from graph-based specifications. The approach is based on the formal meta modeling of visual languages using graph rewriting systems. Besides the syntactical and semantical rules of the language, these meta models include knowledge from the application domains. This enables the resulting tools to provide the user with high level operations for editing, analysis and execution of models. Tools are constructed by generating source code from the meta model of the visual language, which is written in the very high level programming language PROGRES. The source code is integrated into a framework which is responsible for the invocation of commands and the visualization of graphs. As a case study, a visual language for modeling development processes together with its formal meta model is introduced. The paper shows how a process management tool based on this meta model is generated and reports on our experiences with this approach.     

AADL进程子集行为语义研究

AADL是一种基于组件的半形式化建模语言,采用结构化方法对大型复杂软件系统的软硬件进行统一建模,有效描述系统的功能行为、非功能属性以及运行时的体系结构动态演化,但其许多问题需要进一步研究与完善。本文首先分析了AADL形式语义研究现状,然后定义了AADL进程子集的形式语言,建立了AADL进程子集通信模型,通过对事件的形式化定义和分析体现了事件在系统状态转变过程中的重要作用,对AADL进程子集行为语义进行了研究。与相关研究成果的对比说明了本文的优势。本文为AADL语言及其形式语义的发展提供了一种有益的参考,进一步完善大型复杂软件系统体系结构建模与分析技术。     

Language-specific model checking of UML-RT models

Model-driven development (MDD) deals with complexities of modern software development by using models. Their verification is one of the opportunities of MDD, since it can be performed in the early stages of the development. The prevailing trend in verification of MDD models has been to translate them to an input language of one of the existing tools, most notably model checkers. Such an approach has advantages; for instance, we can use tools that achieved a higher level of maturity, including SPIN, NuSMV and Java PathFinder. However, the input languages of model checkers are typically not compatible with MDD models, which can make the translations very complex and difficult to maintain. Moreover, it is more difficult to take advantage of specific features of the structure and semantics of models to, e.g., speed up analysis. In this paper, we depart from the translational trend and present more direct and dedicated approach. We use an MDD language, namely UML-RT (used in IBM Rational Software Architect RealTime Edition), and we introduce a verification method built around its main features such as hierarchical structures, action code and asynchronous communication. In our method we use a formalization tailored to UML-RT models. This enables very easy transformation of models, but also reduces the necessary translations of verification results and directly supports the most important features of UML-RT. The proposed method includes an on-the-fly model checking algorithm based on the original CTL labeling. This algorithm is further optimized to include lazy composition. In the paper, we present all necessary components of the checking algorithms. Additionally, we also show the results of experiments with our implementation using several UML-RT models and CTL formulas. The experiments provide some evidence of the viability of a language-specific analysis of MDD models and of the effectiveness of our optimizations in certain cases.     

双重软件体系结构描述框架XYZ/ADL

体系结构设计在软件开发过程中扮演着重要角色.工程中常用图形语言为软件体系结构建模,它们有直观、半形式化的优点;但是语义不够精确,难以对它们表示的模型进行分析,在这方面,形式化方法可与之互补.但在工程使用中仅用形式化语言建模又不太现实,所以如何结合二者之长以提高软件的可靠性已成为工业界和学术界共同关心的问题.提出了双重软件体系结构描述框架XYZ/ADL:支持工程中软件体系结构的基本概念,前端用一般的体系结构框图作为结构描述,用UML活动图、状态图作为抽象行为表示;后端用既可表示系统动态语义又可表示系统静态语义的时序逻辑语言XYZ/E作为一致的语义基础.前端的图形语言便于软件工程师的交流和使用,后端的形式语言是进一步的形式化分析验证的基础.     

实时UML及其在月球车实时软件开发中的应用

实时UML(UML-RT)是统一建模语言(Unified Modeling Language,UML)在实时系统的扩展和应用,其简洁清晰的面向对象可视化建模方法可以有效解决实时系统中的复杂建模问题;分析了应用实时UML概念和原理进行实时系统可视化建模的问题和方法,并以包含多个子系统的复杂实时系统-月球车系统为例,论述了应用实时UML进行实际软件设计的过程和问题;使用实时UML使得设计过程形象和易于组织,同时方便了项目成员间的交流,大大加快了软件开发的进程。