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

FORMALIZING EXTENDED EVENTS TRACES USING FORMAL SPECIFICATION LANGUAGE Z

作　　者：童翠玲[1] 缪淮扣[1] 刘玲[1] 

机构地区：[1]上海大学计算机工程与科学学院,上海200072

出　　处：《计算机应用与软件》2004年第11期3-5,共3页Computer Applications and Software

基　　金：国家自然科学基金项目(批准号:60 1 730 30 ) ;上海市教委科学与技术发展基金(批准号:0 2AK0 8)资助

摘　　要：软件体系结构被看成是现代软件技术的重要因素之一 ,而一个软件系统结构的关键就是它可以分解成组件和组件交互的规格说明。扩展事件踪迹图 (ExtendedEventsTraces ,EETs)是一种用来描述组件交互的图形技术 ,它允许我们用图来定义结构中经常发生的交互模型 ,并且在多种上下文中可实例化 ,因而可以重用。虽然EETs的图形表示很直观 ,但是语义不够精确 ,因此 ,在本文中将使用形式规格说明语言Z来形式化EETs。并且 。Software architecture is considered as one of the keys to modern software technology,and a crucial aspect of the architecture of a software system is its decomposition into components and the specification of component interactions.Extended Events Traces in a graphical technique for the description of such component interactions.It allows us to define interaction patterns that occur frequently within an architecture,in the form of diagrams.The diagrams may be instantiated in various contexts,thus allowing reuse of interaction patterns.The graphical represent is intuitionistic,but the semantic isn't precise enough.Accordingly,we will formalize EETs using formal specification language Z,and give several examples in the paper.

关 键 词：规格说明 组件 事件 Z语言 交互模型 图形技术 软件体系结构 重要因素 使用形式 形式化 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论] TP391[自动化与计算机技术—计算机科学与技术]