用Z语言形式化扩展事件踪迹图

摘要

软件体系结构被看成是现代软件技术的重要因素之一,而一个软件系统结构的的规格说明.扩展事件踪迹图(Extended Events Traces,EETs)是一种用来描述组件交互的图形技术,它允许我们用图来定义结构中经常发生的交互模型,并且在多种上下文中可实例化,因而可以重用.虽然EETs的图形表示很直观,但是语义不够精确,因此,在本文中将使用形式规格说明语言Z来形式化EETs.并且,给出了形式描述EETs的几个应用例子.