基于状态图转形式化B模型的安全苛求系统开发方法

形式化方法精确且严格,较多应用于安全苛求系统开发,但目前仍存在学习成本高、使用复杂、重用性低等问题。常用的非形式化状态图模型虽易于使用却缺乏严格验证。针对这些问题,提出一种将状态图SCXML模型转译为形式化B模型的模型转化方法,从而结合状态图的易用性降低在安全苛求软件系统开发过程中使用形式化方法的复杂度。该转译方法分为映射规则、同步语义和程序实现3个部分,以保证自动转译后的模型自身含义与基础语义不变。在平交道口控制系统开发案例分析中,该方法根据图元模型自动生成了对应形式化模型,通过对形式化模型的分析改进系统在功能安全、数据安全、隐藏分支3个方面的非安全因素,并保证从需求至模型的一致性,证明了该方法可降低形式化方法建模难度,提高软件系统的正确性、可靠性与安全性。

一种基于Bigraph理论的软件演化过程模型研究

基于Bigraph理论对软件演化过程模型进行研究,目的是能更好地对软件演化过程中相关动态变化进行建模。利用Bigraph理论和软件演化过程的思想,首先提出了一个形式化的软件演化过程模型,然后用扩展的Bigraph来描述软件演化过程模型的结构,使用Bigraph反应系统来描述软件演化过程模型的动态变化,最后对软件演化过程模型动态调整后的完整性进行了验证。

形式化可测性约束在软件模型实现过程中的研究

在软件测试中,软件使用模型反映实际运行场景的能力是直接决定测试的成功与否的关键因素之一。一般可以通过对在需求分析阶段已生成的UML建模进行研究得到使用模型,但原始的UML模型,由于缺乏严格的定义及必要的约束,如果要生成高精度的软件模型,必须对其添加必要的形式化可测性约束。这正是文章研究的重点。

软件形式化与可视化软件模型的转换

It is an important issue in Software Engineering that combined the formal development method with the vi-sual development method. This study is about the transform method and rules between the UML model and theRAISE model. At last try to put this technology and the common software develop process together.

形式化的软件测试模型研究

传统方法中基于软件测试工程师经验的测试用例构造技术使得软件测试的质量很难得到保证。本文提出一种基于形式化方法的软件测试模型。该模型使用形式化描述语言RSL对软件设计进行描述,并在此基础上提出了自动生成软件测试各个阶段所需测试用例的方法框架以及相关实验结论。

一种面向同步交互的软件演化过程建模方法

全球化软件开发导致以交互方式协作开发的频率和复杂性越来越高。为了控制和规范软件演化的开发行为进而提高软件质量,文献[10]设计了软件演化过程元模型EPMM,由EPMM定义的软件演化过程模型未能形式描述其交互的特点。基于EPMM^([10])定义的软件演化过程包括全局层、过程层、活动层和任务层4个抽象层的思想,设计了软件演化过程元模型CEPMM。CEPMM定义的软件演化过程模型可形式描述同步交互的特点是在其活动层,由此提出一种基于通信系统演算(CCS)的软件演化过程活动层的建模方法,然后在Visual Studio平台下实现软件演化过程活动层可视化的建模工具CAmodel。CEPMM构建的软件演化过程活动层模型不仅可以描述并发、迭代等特点,还可以形式描述同步交互的特性,为模型进行严格的数学方法分析、推理奠定了基础。

形式化方法与应用专题前言

随着硬件运算速度变得越来越快、体系结构变得越来越复杂,软件的功能也变得越来越强大而复杂,如何开发可靠的软件系统,已经成为了一项巨大的挑战.形式化方法是利用数学理论与方法论证检验软件系统可靠性与安全性的方法,包括模型检验、定理证明等多种技术手段.近年来,利用形式化方法解决软件可靠性与安全性问题已经获得了越来越广泛的应用.

软件演化过程建模中的开发人员度量方法

提出了一种在构建形式化的软件演化过程模型(formal software evolution process model,FSEPM)中使用X-S图来度量开发人员的统计控制方法。开发人员是构建模型的核心角色,度量其相关属性可以透析和严格管理开发过程。通过一个实例说明如何度量处在构建过程中的开发人员,利用度量结果来分析开发过程的稳定性、找出可归属原因、进行预测和估计、并为整个开发过程的演化奠定基础。

基于OOAPN模型的多代理软件系统的形式化模型

为了增强OOAPN对象的主动性,对OOAPN的通讯机制进行了深入研究。提出了通讯事件的概念,给出了基于OOAPN模型的多代理软件系统的形式化模型,把成熟的面向对象思想、结构化思想以及形式化方法应用于多代理软件系统建模上,提高了OOAPN模型之间的异步通讯能力和复杂系统的建模能力。

软件体系结构讲座 (六)形式化模型和规格说明

本讲讨论软件体系结构的形式化模型和规格说明,即软件体系结构的形式化基础。

浅析软件演化过程描述语言的作用及特点

在整个软件生命周期中,软件演化已成为其中一个日益重要的研究方向.软件演化过程用来建立软件演化的整体任务框架,可以提高软件演化的效率,但其描述力不足,难以在计算机中实现.软件演化过程描述语言作为面向对象的形式化建模语言,其较强的描述力和易于在计算机中实现的特性,使它可以在不同的抽象层次上描述演化过程,且有利于对软件演化过程的控制、分析、度量和改进.

CEPDL:一个简约的软件演化过程建模语言

随着软件演化过程模型被EPMM建模产生,软件演化过程模型的形式验证问题尤其是自动化验证问题却尚未得到解决.为了实现软件演化过程模型的自动化验证,提出了一种简约的软件演化过程建模语言(CEPDL,Concise Software Evolution Process Description Language),定义了CEPDL的语法,并给出了案例研究.CEPDL可以作为模型验证工具的输入语言,能够描述软件演化过程模型,同时描述基于线性时序逻辑的过程模型规约,为最终应用模型检测方法实现对软件演化过程模型的动态性质及行为的验证提供基础.

基于PROMELA模型的安全关键软件形式化验证技术

聚焦安全关键软件,研究基于PROMELA形式模型验证C程序中违反断言、数组越界、空指针解引用、死锁及饥饿等5类故障技术。建立C程序抽象语法树节点到PROMELA模型,验证属性相关函数到PROMELA模型的2类映射规则;根据映射规则提出由C程序自动生成PROMELA形式模型的算法,并对算法进行理论分析;针对C程序中5种故障类型,分别给出基于PROMELA模型的形式化验证方法,并分析验证的范围;覆盖各类故障的验证范围,为每类故障类型选取12个C程序案例进行实证研究,实验结果证明了方法的有效性。

一种安全关键软件系统的形式化开发模型

形式化方法的主要研究对象是计算机系统的设计和验证。近年来,形式化方法的研究扩展到计算机应用系统的各个领域,尤其是安全关键系统。论述了形式化方法对安全关键软件系统的作用,提出了一种安全关键软件系统的形式化开发模型（Safety Critical Software Model-SCSM）,给出了模型的应用实例。

面向对象软件体系结构的形式化模型

软件体系结构设计中的形式化方法 ,一直是软件工程领域中的研究热点 .而在面向对象环境中如何对体系结构进行形式化 ,以精确描述其静态结构与动态交互行为 ,则一直未有好的解决办法 .本文使用符号逻辑方法描述面向对象系统中的基本组成单元 。

软件体系结构模型的形式化研究．

本文用软件体系结构描述语言WRIGHT对三层C/S模型进行形式化描述,指出这种描述的优点以及软件体系结构模型形式化研究的重要性.

面向同步交互的软件演化过程全局层和过程层的建模

在全球化软件开发的背景下,针对分布在不同地域的开发团队频繁同步交互式所引起的软件演化过程的可信问题,和软件演化过程元模型EPMM构建的软件演化过程模型描述的同步交互是非形式化的问题,提出了使用通信系统演算CCS为形式工具的分布式软件演化过程元模型CEPMM.基于CEPMM构建分布式软件演化过程多层模型,包括全局层、过程层、活动层及任务层:任务是原子的,不可分割;为建立分布式软件演化过程全局层和过程层模型提出一种建模方法;最后为实现基于EPMM建模到基于CEPMM建模全局层和过程层转化,在Visual Studio平台下使用C#语言研发出工具CLPmodel.结果表明:全局层和过程层模型的建立,为在该粒度上对分布式软件演化过程的可信分析与研究奠定基础.

通过模型比较构造软件演化的过程模型

为了得到软件系统的演化过程模型,引入了工作模型的概念用以描述软件的工作过程。通过建立起软件演化前后的工作模型并对其进行比较,可以得到由旧的工作模型向新的工作模型转化需要执行的各种活动,这样的活动通过在软件的代码、数据和文档三个层面的映射便具有了实际意义,以此为基础所构造的演化活动图能够最终转换为Petri网形式的演化过程模型。

基于CHAM的软件连接件形式化模型

软件连接件是软件体系结构中的一个重要概念 ,是构件间相互作用的媒体。用形式化方法对其模型加以描述是软件体系结构研究中的一个重点。化学抽象机形式化语言 (CHAM :ChemicalAbstractMachine)是一种通用的、简单直观的计算模型描述语言。本文在分析了连接件语义模型的基础上 ,提出了一种基于CHAM的软件连接件描述模型 ,从软件连接件静态组成及动态行为两个方面对连接件进行形式化、规范化地描述和分析 ,以期进一步实现简化软件连接件的设计、增强其通用性的目的。

一种基于形式化B方法的软件构件模型

提出了一种基于形式化B方法的软件构件模型,分基于检索的部分、基于学习的部分和基于组装与演化的部分来依次展现构件信息,并结合实例给出了使用B语言来描述构件的具体功能和行为规约的具体运用。