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

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

设备自动巡检控制逻辑的层级时间自动机建模与验证

地下建筑工程中的设备系统经常处于静止状态,为保证其在需要时能安全可靠地运行,需对设备进行定期的自动巡检。在自动巡检的过程中,设备自动巡检控制逻辑起到了举足轻重的作用。为了解决复杂的设备自动巡检控制逻辑造成的一系列问题,之前提出了一种层级有限自动机(HFA)的形式化模型,并利用HFA对设备自动巡检控制逻辑实现了行为建模,但并未添加时间属性,也未验证其正确性与可靠性。现提出一种层级时间自动机形式化模型,并利用它对设备自动巡检控制逻辑进行建模,再利用UPPAAL对其进行分析与形式化验证,分别验证其安全性、可达性、活性及时间约束,以此来确保其时效正确性与可靠性。这种建模与形式化验证方法弥补了之前无时间约束的漏洞,有效确保了设备自动巡检控制逻辑的正确性与可靠性。最终,该模型通过了模拟和验证,这充分证明了设备自动巡检控制逻辑是正确可靠的。     

基于GEP算法的高阶常微分方程预测模型

针对动态系统预测建模中建模效率低,无显式模型的缺陷。提出一种基于基因表达式编程（GEP）的高阶常微分方程预测模型（GEP-HODE）。将一维数据的变化特性使用高阶微分进行表示,通过GEP对高阶微分数据进行建模,得到显式模型。对高阶常微分方程模型进行降阶处理,使用数值方法进行求解,得到预测值。该方法利用了GEP算法“基因型-表现型”的编码特性,实现了模型建立与参数优化的同步,大幅度提升建模效率。以太阳黑子年平均数作为实验数据建模预测,结果表明,该方法相比GP混合建模方法有更高的效率,相比混合BP神经网络模型等方法有更好的精度。     

基于时间STM的软件形式化建模与验证方法

状态迁移矩阵(state transition matrix,简称STM)是一种基于表结构的状态机建模方法,前端为表格形式,后端则具有严格的形式化定义,用于建模软件系统行为.但目前STM不具有时间语义,这极大地限制了该方法在实时嵌入式软件建模方面的应用.针对这一问题,提出了一种基于时间STM(time STM,简称TSTM)的形式化建模方法,通过为STM各单元格增加时间语义和约束,使其适用于实时软件行为刻画.此外,针对TSTM给出了一种基于界限模型检测(bounded model checking,简称BMC)技术的时间计算树逻辑(time computation tree logic,简称TCTL)模型检测方法,以验证TSTM时间及逻辑属性.最后,通过对某型号列控制软件进行TSTM建模与验证,证明了上述方法的有效性.     

基于形式化方法的有限域乘法器的建模与验证

针对有限域乘法器设计正确性的问题进行研究,阐述了有限域乘法器在高阶逻辑定理证明器HOL4中进行形式化建模和验证的过程。通过分析电路的结构特性和时序特性,提出了结合层次化和基于周期的形式化建模方法,构建4位多项式基有限域乘法器的形式化模型;最后在HOL4系统中完成对其相关性质的验证。实验结果证明了该有限域乘法器设计的正确性,同时表明所提出的建模方法对时序逻辑电路的验证是有效的。     

基于XYZ/SE的软件部分正确性验证

针对软件形式化描述和正确性验证研究中存在的问题,提出了基于XYZ/SE的统一框架研究该问题。在该框架下,基于逐步求精思路对软件进行抽象;对软件整体进行形式化描述和部分正确性验证;对抽象得到的软件各部分进行形式化描述和部分正确性验证;进行调整和验证,即：如果推导结果与预期不一致,则需要重写相关程序或者回溯检查推导过程是否存在错误,直至程序部分正确性得到验证为止。以国库信息处理系统为对象,分析了基于XYZ/SE的统一框架性能。分析表明,基于该框架能够对软件的不同抽象层次进行规范描述,实现从抽象（静态语义）到具体（动态语义）的平滑过渡。同时,基于XYZ/SE的统一框架也可以表示Hoare逻辑推演规则。     

基于面向方面的实时系统建模方法

分布式实时系统的实时特性可以利用面向方面软件设计方法来建模，把时间方面细分为确定的时间子方面、不确定的时间子方面和模糊时间子方面。根据面向方面技术，不同的时间子方面分别利用随机实时时序逻辑（SQTL）和模糊时间Petri网（FTN）来表示，并且每个不同形式化语言表示的子方面模型能够通过转化为时间自动机织入系统，实现系统的实时特性。     

SpaceWire译码电路在HOL4中的形式化验证

SpaceWire是在苛刻环境下的高速通信总线协议,译码电路是其接收端的关键电路,对该电路进行形式化验证具有重要的现实意义.形式化验证方法中的定理证明将需要分析的电路进行形式化建模,结合定理证明器,对模型的性质进行严格推理从而完成验证.本文运用定理证明的方法,在高阶逻辑证明工具HOL4中对SpaceWire总线的译码电路进行形式化验证.首先根据SpaceWire标准规范抽取相关性质,用高阶逻辑语言形式化描述;然后分析电路设计中的VHDL代码,依据代码实现的功能用相应的逻辑谓词建模;最后在HOL4中证明了译码电路设计的模型能满足所提取的性质.本文同时给出了形式化建模的方法和验证过程.     

基于系统理论过程分析的软件安全性需求分析与验证方法

针对传统系统理论过程分析（STPA）方法缺乏自动化实现手段、自然语言结果分析存在歧义性的问题,提出一种基于STPA的软件安全性需求分析与验证方法。首先,提取软件安全性需求,并利用算法将其转化为形式化表达式;其次,建立状态图模型来描述软件安全控制行为逻辑,并将其转化为程序可读的形式化语言;最后,采用模型检验技术进行形式化验证。结合某武器发射控制系统案例验证了方法的有效性,结果表明,该方法能够实现安全需求分析的自动化生成与形式化验证,解决了传统方法对于人工干预的依赖问题及自然语言描述问题。     

基于时序描述逻辑的Web服务本体语言过程模型语义

针对Web服务本体语言(OWL-S)过程模型存在动态交互和时序特征表达能力不足的问题,提出一种基于时序描述逻辑的过程模型形式化方法。通过对OWL-S过程模型的原子过程和组合过程语义进行形式化的描述,得到了OWL-S的过程模型的动态语义,最终实现了对OWL-S过程模型的形式化建模。实例结果验证了所提方法的可行性,为进一步的分析和验证提供了基础。     

基于扩展WF-Net的配电网故障诊断与抢修流程优化

基于扩展WF-Net对配电网故障诊断与抢修流程进行了建模与优化。首先将流程涉及的信息系统封装成具有松散耦合特性的 IT 服务;然后扩展了 WF-net 的时间集和颜色集,提出了基于 IT 服务的赋时有色工作流网（TCWFN-ITS）,以显式地表达业务流程与IT服务的调用关系。最后,针对某电力公司配电网故障诊断与抢修流程,采用TCWFN-ITS进行建模,使用Petri网建模工具CPN Tools进行仿真分析,通过并行执行任务、合并任务、优化服务占用端口数量等手段,实现了配电网故障诊断与抢修流程性能提升和 IT 服务的平衡配置,验证了所提方法的可行性和有效性。     

Proving properties of real-time systems through logicalspecifications and Petri net models

Addresses the problem of formally analyzing the properties of real-time systems. We propose a method based on modeling the system as a timed Petri net and on specifying its properties in TRIO, an extension of temporal logic suitable for dealing explicitly with time and for measuring it. Timed Petri nets are axiomatized in terms of TRIO, so that their properties can be derived as theorems in the same spirit as the classical Hoare method allows one to prove properties of programs coded in a Pascal-like language. The method is also illustrated through an example     

FAME: A UML-based framework for modeling fuzzy self-adaptive software

Context: Software Fuzzy Self-Adaptation (SFSA) is a fuzzy control-based software self-adaptation paradigm proposed to deal with the fuzzy uncertainty existing in self-adaptive software. However, as many software engineers lack fuzzy control knowledge, it is difficult for them to design and model this kind of fuzzy self-adaptive software (F-SAS). Therefore, efficient and effective modeling technologies and tools are needed for the SFSA framework.Objective: This paper aims to identify modeling requirements of F-SAS and to provide a modeling framework to specify, design and model F-SAS systems. Such a framework can simplify modeling process of F-SAS and improve the accessibility of software engineers to the SFSA paradigm.Method: This study proposes a modeling framework called Fuzzy self-Adaptation ModEling (FAME). By extending UML, FAME creates three types of modeling views. An analysis view called Fuzzy Case Diagram is created to specify the fuzzy self-adaptation goal and the realization processes of this goal. A structure view called Fuzzy Class Diagram is created to describe the fuzzy concepts and structural characteristics of F-SAS. A behavior view called Fuzzy Sequence Diagram is created to depict the dynamic behaviors of the F-SAS systems. The framework is implemented as a plug-in of Enterprise Architect.Results: We demonstrate the effectiveness and efficiency of the proposed approach by carrying out a subject-based empirical evaluation. The results show that FAME framework can improve modeling quality of F-SAS systems by 44.38% and shorten modeling time of F-SAS systems by 38.41% in comparison with traditional UML. Thus, FAME can considerably ease the modeling process of F-SAS systems.Conclusion: FAME framework incorporates the SFSA concepts into standard UML. Therefore, it provides a direct support to model SFSA characteristics and improves the accessibility of software engineers to the SFSA paradigm. Furthermore, it behaves a good example and provides good references for modeling domain-specific software systems.     

Modelling temporal behaviour in complex systems with Timebands

Complex real-time systems exhibit dynamic behaviours on many different time levels. To cope with the wide range of time scales and produce more dependable computer-based systems, we develop a Timebands model that can explicitly recognise a finite set of distinct time bands in which temporal properties and associated behaviours are described. In order to formalise the Timebands model, we propose a new timed model, named Timed Circus, of Circus, which is the combination of Z, CSP, and the refinement calculus in the setting of Unifying Theories of Programming. Different from most approaches such as Timed CSP, Timed Circus uses a complete lattice in the implication ordering to model the distinctive features of the Timebands model. As a result, the semantics of the Timebands model is built upon Timed Circus to guarantee soundness of each operator and maintain consistency and coordination between different time bands. By means of two small systems, we demonstrate how the Timebands model contributes to describing complex real-time systems with multiple time scales.     

面向软件模糊自适应的UML用例扩展

现有统一建模语言(UML)设施及一般软件自适应工具难以直接支持软件模糊自适应(SFSA)需求分析与设计阶段的建模,为此,提出一种基于UML用例扩展的SFSA需求分析与设计方法--Fuzzy Case。该方法结合SFSA的概念模型,应用UML扩展机制引入新的构造型和标记值,建立了Fuzzy Case的一般模型;同时定义了Fuzzy Case的语法结构,并用对象约束语言(OCL)定义了其语义描述,形成了完整的SFSA建模设施。实例验证表明,与传统方法相比,Fuzzy Case能更清晰地表达SFSA的结构,准确定义软件的内部语义,建模过程更加简单方便,能有效提高SFSA的开发效率。     

Active and dynamic information fusion for facial expression understanding from image sequences

This paper explores the use of multisensory information fusion technique with dynamic Bayesian networks (DBN) for modeling and understanding the temporal behaviors of facial expressions in image sequences. Our facial feature detection and tracking based on active IR illumination provides reliable visual information under variable lighting and head motion. Our approach to facial expression recognition lies in the proposed dynamic and probabilistic framework based on combining DBN with Ekman's facial action coding system (FACS) for systematically modeling the dynamic and stochastic behaviors of spontaneous facial expressions. The framework not only provides a coherent and unified hierarchical probabilistic framework to represent spatial and temporal information related to facial expressions, but also allows us to actively select the most informative visual cues from the available information sources to minimize the ambiguity in recognition. The recognition of facial expressions is accomplished by fusing not only from the current visual observations, but also from the previous visual evidences. Consequently, the recognition becomes more robust and accurate through explicitly modeling temporal behavior of facial expression. In this paper, we present the theoretical foundation underlying the proposed probabilistic and dynamic framework for facial expression modeling and understanding. Experimental results demonstrate that our approach can accurately and robustly recognize spontaneous facial expressions from an image sequence under different conditions.     

Specification and automated validation of staged reconfiguration processes for dynamic software product lines

Dynamic software product lines (DSPLs) propose elaborated design and implementation principles for engineering highly configurable runtime-adaptive systems in a sustainable and feature-oriented way. For this, DSPLs add to classical software product lines (SPL) the notions of (1) staged (pre-)configurations with dedicated binding times for each individual feature, and (2) continuous runtime reconfigurations of dynamic features throughout the entire product life cycle. Especially in the context of safety- and mission-critical systems, the design of reliable DSPLs requires capabilities for accurately specifying and validating arbitrary complex constraints among configuration parameters and/or respective reconfiguration options. Compared to classical SPL domain analysis which is usually based on Boolean constraint solving, DSPL validation, therefore, further requires capabilities for checking temporal properties of reconfiguration processes. In this article, we present a comprehensive approach for modeling and automatically verifying essential validity properties of staged reconfiguration processes with complex binding time constraints during DSPL domain engineering. The novel modeling concepts introduced are motivated by (re-)configuration constraints apparent in a real-world industrial case study from the automation engineering domain, which are not properly expressible and analyzable using state-of-the-art SPL domain modeling approaches. We present a prototypical tool implementation based on the model checker SPIN and present evaluation results obtained from our industrial case study, demonstrating the applicability of the approach.     

Controller synthesis for dynamic hierarchical real-time plants using timed automata

We use timed I/O automata based timed games to synthesize task-level reconfiguration services for cost-effective fault tolerance in a case study. The case study shows that state-space explosion is a severe problem for timed games. By applying suitable abstractions, we dramatically improve the scalability. However, timed I/O automata do not facilitate algorithmic abstraction generation techniques. The case study motivates the development of timed process automata to improve modeling and analysis for controller synthesis of time-critical plants which can be hierarchical and dynamic. The model offers two essential features for industrial systems: (i) compositional modeling with reusable designs for different contexts, and (ii) state-space reduction technique. Timed process automata model dynamic networks of continuous-time communicating plant processes which can activate other plant processes. We show how to establish safety and reachability properties of timed process automata by reduction to solving timed games. To mitigate the state-space explosion problem, an algorithmic state-space reduction technique using compositional reasoning and aggressive abstractions is also proposed. In this article, we demonstrate the theoretical framework of timed process automata and the effectiveness of the proposed state-space reduction technique by extending the case study.