软件形式化建模方法探析

周建儒（四川信息职业技术学院，四川广元628040）



软件形式化建模方法探析

周建儒
（四川信息职业技术学院，四川广元628040）

摘要：传统软件开发流程存在各种缺陷。软件形式化方法是建立在严格数学基础上的软件开发方法，该方法为从根本上解决传统软件开发过程中存在的主要缺陷提供了可能，其中Pi验算就是比较典型的一种形式化语言，结合实例来分析Pi验算进行形式化建模的过程，可以帮助我们更好地了解这种形式化语言建模方式。

关键词：软件形式化；Pi验算；软件工程；建模方式

1　引言

在传统的软件开发中，往往会出现项目延迟、预算超支、后期发现软件缺陷等问题，从而花费高额代价进行修复。分析导致软件事故的诸多原因，我们发现很难从根本上解决软件开发方式所带来的问题，因为前期成果是用自然语言编写的文档，如需求规格说明书、设计说明书等，最后的成果是形式化的程序。文档是完全非形式化的表达，只能由人阅读和理解，难以通过自身的语义来证明其表达流程的正确性。而形式化的程序有严格的定义和语义［1］。程序的所有静态和动态性质都蕴藏在系统代码中，且程序包含过多的实现细节和语言细节，进行验证的成本很高。需求和设计与最终实现的程序的一致性难以判定［2］。测试发现问题的能力很有限，不能成为评判软件质量好坏的标准。因此，如果把前期的需求流程也完全通过严格的形式化语言来表述，那么会很容易保证需求和最终代码的一致性。因此，形式化方法与理论在软件的发展中显得尤其重要。目前研究较多的形式化语言有Petri网和Pi验算，而Pi验算因为其具备传输通道的能力，从而更适应一些需求变化较大的场合。本文以形式化语言Pi验算为例，探讨形式化语言的建模方式。

2　形式化建模方法浅析

2.1 Pi演算概述

形式化方法是基于严格定义的数学概念和语言［3］，语义清晰，无歧义。可以用自动化或半自动化的工具进行检查和分析。事实上，软件开发正在从朴素的、非形式的设计方法，向着更加严格定义、更加形式化的方向转变。形式化方法研究如何把通过严格的数学基础定义需求的方式引入软件开发的各阶段。

Pi演算于上世纪80年代末由图灵得主Robin Milner提出，是一种描述和分析并发系统的演算模型，用演算中的归约表示由进程间的相互通信形成的动态演化。在Pi演算中最基本的元素是名字，名字有无穷多，记作：x，y，…∈Name；再一个概念就是进程，进程是由名字按照下述语法构成的表达式：

进程P：=P|Q|M|！P|（Vx）P

其中P|Q|M称为并行，解释为独立并行执行的进程，它们之间可以通过通道通信；！P称为重复（replication），即一个系统中有多个进程P在并行执行；（Vx）P称为变量的限制，即把变量x绑定在进程P中。

2.2 Pi验算描述流程

在所有的业务流程中，都有信息的接收与发送，可以通过Pi验算［3］描述最基本的业务流程。首先看看简单的发送和接收模型如何通过Pi验算描述，发送消息模型如图1所示。

Pi演算表达消息发送模式如下：

图1　消息发送

其中，X代表一个进程，A代表进程中的一个任务，msg代表信息，m代表发送信息的管道。

接收消息模式如图2所示。一个进程收到一个来自另一个进程的消息。

图2　消息接收

Pi演算表达消息接收模式如下：

其中，X代表一个进程，A代表进程中的一个任务，msg代表信息，m代表接收信息的管道。

为了进一步演示Pi演算描述流程的效果，这里整合发送和接收两个模式，通过Pi演算来描述并通过移动工作平台验证交互模型。假设有两个进程X1、X2，通道ch1发送信息，通道ch2接收信息。流程如图3所示。

图3　消息交互

X1组织中，两个任务实体表示如下：

X2组织中，两个任务实体表示如下：

其中组织X1和X2分别定义如下：

2.3流程的验证

通过以上分析，完成了交互流程的Pi验算表达，现在把Pi验算的代码转换成mwb语法的代理对象，转换后的具体代理对象共有三个，即agent X1、agent X2、agent P，具体代码如下所示：

agent X1

X1（ch1，ch2，x1，msg，req，res）='ch1.'x1< msg>.x1（msg）.ch2（res）.0

agent X2

X2（ch1，ch2，x2，mes，req，res）=ch1（req）.'x2< mes>.x2（mes）.'ch2.0

agent P

P（ch1，ch2，x1，x2，msg，mes，req，res）=X1 （ch1，ch2，x1，msg，req，res）|X2（ch1，ch2，x2，mes，req，res）

把这三个代理对象保存在文件pro.ag中，启动移动工作平台，导入pro.ag文件并查看代理对象，具体如图4所示。

图4　查看流程代理对象

从图4中可以看出，代理对象一共有三个，因为模拟X1和X2两个对象没有多大意义，因此，这里模拟对象P，输入step P（ch1，ch2，x1，x2，msg，mes，req，res），如图5所示。

连续选择一条路径，得到的结果如图6所示。

从图6中可以清楚地看到，移动工作平台模拟了代理P的整个交互过程。

图5　模拟对象P

图6　跟踪代理P的交互过程

3　结论

通过分析传统的软件开发所带来的软件缺陷，得出传统软件开发方法难以从根本上解决这些问题。伴随着形式化方法的发展，为从本质上解决软件开发过程中存在的问题带来了希望，形式化方法能保证从软件需求到软件编码整个流程的逻辑一致性。然而形式化方法目前尚未普及，接下来的工作需要进一步研究工作流引擎与形式化方法的结合［4］，让形式化方法更好地应用于软件系统的开发。

参考文献：

［1］张广泉.关于软件形式化方法［J］．重庆师范学院学报，2002（2）：35-36.

［2］吕毅.形式化方法介绍及其在工程中的应用［J］．微电子学与计算机，2003（10）：78-79.

［3］杨鹏玉.基于Pi演算的BPMN编排模式［J］.计算机工程，2009，35（23）：274-278．

［4］李占峻.应用Pi演算描述工作流高级模式［J］.信息工程大学学报，2009，10（4）．

Software Formalization Modeling Analysis

ZHOU Jian-ru
（Sichuan Information Technology College，Sichuan Guangyuan 628040，China）

Abstract:There are various defects in traditional software development process. Built on the basis of strict mathematical software development software formalization provides methods to solve the defects in traditional software development process from the fundamental flaws. Pi checking is a typical formalization language. The paper analyzes it’s modeling process with examples.

Key words:software formalization；Pi checking；software engineering；modeling method

中图分类号：TP311.5

文献标志码：A

文章编号：1673-2022（2016）02-0048-03

收稿日期：2015-12-28

作者简介：周建儒（1980-），男，陕西城固人，讲师，硕士，研究方向为软件工程。