基于UPPAAL的AADL模型可调度性验证

针对体系结构分析设计语言(AADL)模型的可调度性验证问题,提出了利用模型检测工具UPPAAL对其线程组件在非抢占型调度策略下的可调度性进行形式化分析和验证的方法,并实现了从AADL模型到UPPAAL中模型的模型转换工具。实验结果证明了通过UPPAAL来分析和验证AADL模型的可调度性问题的可行性。相比其他方法而言,基于形式化理论的本方法的验证结果更加精确。     

Timed Behavior Trees for Failure Mode and Effects Analysis of time-critical systems

Behavior Trees are a graphical notation used for formalising functional requirements, and have been successfully applied to several industrial case studies. However, the standard notation does not support the concept of time, and consequently its application is limited to non-real-time systems. To overcome this limitation we extend the notation to timed Behavior Trees. We provide an operational semantics which is based on timed automata, and thus serves as a formal basis for the translation of timed Behavior Trees into the input notation of the timed model checker UPPAAL. System-level timing properties of a Behavior Tree model can then be automatically verified using UPPAAL. Based on the notational extensions with model checking support, we introduce timed Failure Mode and Effects Analysis, a process for identifying cause-consequence relationships between component failures and system hazards in real-time safety critical systems.     

Verification of real‐time systems design

The main objective of this paper is to present an approach to accomplish verification in the early design phases of a system, which allows us to make the system verification easier, specifically for those systems with timing restrictions. For this purpose we use RT‐UML sequence diagrams in the design phase and we translate these diagrams into timed automata for performing the verification by using model checking techniques. Specifically, we use the Object Management Group's UML Profile for Schedulability, Performance, and Time and from the specifications written using this profile we obtain the corresponding timed automata. The ‘RT‐UML Profile’ is used in conjunction with a very well‐known tool to perform validation and verification of the timing needs, namely, the UPPAAL tool, which is used to simulate and analyze the behaviour of real‐time dynamic systems described by timed automata. Copyright © 2009 John Wiley & Sons, Ltd.     

TCBV:一种构件时序行为建模与相容性验证工具

利用形式化方法对复杂实时构件系统的时序行为进行建模与验证对于提高安全攸关实时构件系统的正确性、可靠性与安全性具有重要意义。介绍了基于时间行为协议的构件时序行为的形式化建模和相容性验证方法,给出了时间行为协议建模与相容性验证工具TCBV的系统架构与功能模块。TCBV应用方便,能够实现实时构件时序行为模型的图形化表示,并可对复杂交互行为的相容性进行自动验证。结合应用实例,介绍了如何利用TCBV对复杂实时构件系统的时序行为进行建模和验证。最后,将TCBV与其它相关工具进行了比较。     

Integrating UML and UPPAAL for designing, specifying and verifying component-based real-time systems

A new tool for integrating formal methods, particularly model checking, in the development process of component-based real-time systems specified in UML is proposed. The described tool, TANGRAM (Tool for Analysis of Diagrams), performs automatic translation from UML diagrams into timed automata, which can be verified by the UPPAAL model checker. We focus on the CORBA Component Model. We demonstrate the overall process of our approach, from system design to verification, using a simple but real application, used in train control systems. Also, a more complex case study regarding train control systems is described.     

Transformation of Function Block Diagrams to UPPAAL timed automata for the verification of safety applications

Verification of IEC 61131-3 based safety applications is a challenge in the industrial automation domain. In this paper, the transformation of FBD diagrams to UPPAAL formal models was adopted to address this challenge. A set of transformation rules are defined for the automatic transformation of IEC 61131-3 Function Block based safety applications to UPPAAL timed automata models. These models are next used for the verification of the safety application. Both the source and the target domain models have been formally defined and these definitions are used for the definition of the transformation rules. Based on this a prototype model transformer was developed using Java. The transformer was used with various safety applications to check the efficiency of the transformation process. A laboratory system is presented as a case study to highlight the proposed approach.     

一种软件自适应UML建模及其形式化验证方法

软件自适应的建模和形式化验证是提高自适应软件开发效率、保证自适应软件可靠性的基础,现有研究中软件自适应可视化建模与形式化建模相隔离,一定程度上阻碍了自适应软件的开发.为此,提出MV4SAS的方法,将可视化的UML与严格化的时间自动机相结合,用于软件自适应的建模和形式化验证.首先,应用UML扩展机制引入新的构造型、标记值和约束条件,定义软件自适应建模设施,在此基础上构造软件自适应结构模型和行为模型;然后,根据定义好的转换算法将软件自适应行为模型转换为时间自动机网络,建立软件自适应形式化模型;最后,定义一组软件自适应形式化验证性质,并利用模型检测工具UPPAAL验证软件自适应模型的可靠性.案例研究表明,该方法可有效降低软件自适应建模和验证的复杂度,提高软件自适应的建模效率和模型可靠性.     

构件式实时系统建模与验证研究

在复杂的实时系统开发中使用构件式设计方法已成为目前软件开发领域中的研究热点,如何有效地验证实时软件的设计是否满足给定的时间需求并降低验证过程的复杂度,是实时计算领域中的主要挑战之一.文中对构件接口模型进行时间扩展,提出了时间接口模型,并将其用于构件接口交互行为的形式化建模.在接口自动机理论的的基础上进一步提出了时间接口自动机模型用于描述时间接口交互下构件的行为及组合方法,通过消除错误状态产生组合模型来约减构件时间接口自动机模型的积,并在约减的模型上进行性质检验,降低了分析复杂度,有效地应对状态空间爆炸问题.为了说明论文建议的方法,详细讨论了一个简单的、贯穿整篇论文的示例系统.     

移动支付协议PCMS的形式化分析和验证

移动电子商务协议的形式化分析和验证是近年来移动电子商务协议的一个重要研究热点。以一个支付网关为中心的匿名的移动电子商务支付协议PCMS为研究对象,建立了PCMS协议的时间自动机模型,并用计算树逻辑CTL公式描述PCMS协议的部分性质,最后利用模型检测工具UPPAAL对PCMS协议的无死锁、时效性、有效性和钱原子性进行检测验证。验证结果表明,以支付网关为中心的匿名的安全支付协议PCMS满足无死锁、时效性、有效性和钱原子性。     

构件行为协议实时性扩展及相容性验证

对复杂实时构件系统行为进行形式化描述和相容性验证,可以有效提高系统的正确性、可靠性。分析了学术界和工业界的主流构件模型及常见时间行为的形式化描述方法,对构件行为协议BP(Behavior Protocol)进行了扩展,提出了时间行为协议TbP(Timed Behavior Protocol),分析了构件组合中常见的相容性错误类型,给出了基于时间行为协议的构件组合相容性验证算法。TBP应用简洁、方便、易于验证。结合具体例子给出了应用示例。     

基于UPPAAL的实时系统模型验证

UPPAAL是一种使用时间自动机模型的实时系统验证工具，它可以避免时间自动机求积时状态空间的爆炸。介绍了时间自动机理论和工具UPPAAL，着重说明如何用UPPAAL进行模型检查，并给出了一个应用实例。     

UPPAAL--一种适合自动验证实时系统的工具

UPPAAL是一个基于时间自动机的自动验证工具,已成功地用于实时控制器和通信协议等实时系统的验证.本文介绍了UPPAAL的语法,语义和语用,列举了它的几种扩展形式,并归纳了其应用及研究现状.     

智能合约的时间约束模式及其形式化验证

智能合约是一套以数字形式定义的承诺.通过智能合约可以大大减少协议制定的中间环节, 提高协议制定的效率.区块链技术为智能合约的执行提供了可信平台.随着区块链应用的拓广与深入, 智能合约的作用必然越来越突出, 智能合约的可靠性问题也将更加突显.以提高智能合约可靠性为目的的研究日益得到重视, 但尚未有人对智能合约的时间性质可能引起的可靠性问题进行过系统的研究.本文通过分析典型智能合约, 对智能合约时间约束的不同表现形式进行梳理, 提炼出相应的时间约束模式并对其进行形式化; 定义Solidity智能合约到时间自动机的转换规则并实现其到实时模型检测工具UPPAAL入口模型的自动转换; 再利用UPPAAL验证合约的时间相关性质.最后对两个实际合约进行实例研究, 结果表明本文所提炼模式的普遍性以及本文所提出形式化验证方案的可行性和有效性.     

Formal verification of components assembly based on SysML and interface automata

We propose an approach which combines component SysML models and interface automata in order to assemble components and to verify formally their interoperability. So we propose to verify formally the assembly of components specified with the expressive and semi-formal modeling language, SysML. We specify component-based system architecture with SysML Block Definition Diagram, and the composition links between components with Internal Block Diagrams. Component’s protocols are specified with sequence diagrams, they are necessary to exploit interface automata formalism. Interface automata is a common Input Output (I/O) automata-based formalism intended to specify the signature and the protocol level of the component interfaces. We propose formal specifications for SysML semi-formal models in order to exploit interface automata approach. We also improve the interface automata approach by considering system architecture, specified with SysML, in the verification of components composition.     

An I/O Automata-based Approach to Verify Component Compatibility: Application to the CyCab Car

An interesting formal approach to specify component interfaces is interface automata based approach, which is proposed by L. Alfaro and T. Henzinger. These formalisms have the ability to model both the input and output requirements of components system. In this paper, we propose a method to enrich interface automata by the semantics of actions in order to verify components interoperability at the levels of signatures, semantics, and protocol interactions of actions. These interfaces consist of a set of required and offered actions specified by Pre and Post conditions. The verification of the compatibility between interface automata reuse the L. Alfaro and T. Henzinger proposed algorithm and adapt it by taking into account the action semantics. Our approach is illustrated by a case study of the vehicle CyCab.     

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

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

模型驱动的嵌入式系统设计安全性验证方法研究

基于模型的嵌入式系统安全性分析与验证方法是近年来在安全攸关系统工程领域中出现的一个重要研究热点。提出一种基于模型驱动架构的面向SysML/MARTE状态机的系统安全性验证方法,具体包括:构建了具备SysML/MARTE扩展语义的状态机元模型,以及安全性建模与分析语言AltaRica的语义模型GTS的元模型;然后建立了从SysML/MARTE状态机模型分别到时间自动机模型以及AltaRica模型的语义映射模型转换规则,并基于AMMA平台和时间自动机验证工具UPPAAL设计实现了对SysML/MARTE状态机的模型转换与系统安全性形式化验证的框架。最后给出了一个飞机着陆控制系统设计模型的安全性验证实例分析。     

Verification of Asynchronous Circuits using Timed Automata

In this work we apply the timing verification tool OpenKronos, which is based on timed automata, to verify correctness of numerous asynchronous circuits. The desired behavior of these circuits is specified in terms of signal transition graphs (STG) and we check whether the synthesized circuits behave correctly under the assumption that the inputs satisfy the STG conventions and that the gate delays are bounded between two given numbers. Our results demonstrate the viability of the timed automaton approach for timing analysis of certain classes of circuits.