一种验证软件演化过程行为的代数推导方法

针对现有软件过程验证主要以结构验证和性质验证为主,缺乏行为验证的不足,提出了一种验证软件演化过程行为的代数方法.该方法使用通信进程代数ACP对软件演化过程元模型EPMM进行扩展,提出软件演化过程元模型代数EPMM-A.针对EPMM建模产生的软件演化过程模型,一方面使用EPMM-A形式定义软件演化过程模型的行为规约,另一方面在其公理系统的支持下,基于等式推导验证软件演化过程模型的行为与行为规约是否一致,使行为验证方式从模型推导(非形式化)变为代数推导(形式化).为了说明代数推导的正确性,证明了软件演化过程元模型代数的公理系统具有可靠性.

基于进程代数的Yahalom协议正确性的形式化验证

通信过程中为了使得通信双方之间的对话过程是安全传输的,在引入可信第三方的基础上,Yahalom协议借助于可信第三方为通信双方分配"好"的会话密钥,利用该共享密钥加密对话内容保证双方对话的安全。Yahalom协议的形式化验证具有很重要的意义。为了使可信第三方在通信双方之间安全地分配会话密钥,文中对通信过程进行理论化形式的验证。文中基于可信平台的随机会话密钥分配过程进行了抽象化的处理,给出了抽象模型中各个实体状态及状态变迁的操作语义描述,建立了Yahalom协议结构化的操作语义并发计算模型,主要通过ACP公理系统对Yahalom协议的状态变迁系统进行了形式化的验证,验证结果表明Yahalom协议系统地展示了期望的外部行为,从理论上证明了基于进程代数的Yahalom协议是可行的。