%0 Journal Article
%T Compositional Semantics and Refinement of Statecharts<br>Statecharts的组合语义与求精
%A ZHU Xue-Yang
%A TANG Zhi-Song
%A <br>朱雪阳
%A 唐稚松
%J 软件学报
%D 2006
%I 
%X 由于简洁、直观的表达能力,Statecharts被用于许多反应系统的行为建模.Statecharts可表示不同抽象层次的系统行为,因而可用来表示逐步求精建模中各步的结果.但对于求精过程中下层是否保持了上层的语义、所建模型是否满足某些性质的问题,却难以在其自身的框架下进行讨论.在这方面,形式化语言XYZ/E可与其互补.XYZ/E是一种可执行线性时序逻辑语言,既可表示系统的性质,又可表示系统的行为.递归地在基本迁移系统上解释Statecharts语义,用XYZ/E公式表示它的时序语义.这一语义是模块级可组合的.求精过程的语义保持,可直接从语义定义得到保证.Statecharts所描述的系统行为模型和性质在同一个逻辑中表示,因此,系统行为是否满足所需性质的问题可由逻辑蕴涵式表示.
%K Statecharts
%K XYZ/E<br>时序逻辑
%K 形式语义
%K 组合
%K 求精
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=AD40E9FCA4E90668&yid=37904DC365DD7266&vid=BCA2697F357F2001&iid=E158A972A605785F&sid=2B6C525BCE31A7DA&eid=8243B77967FFD12E&journal_id=1000-9825&journal_name=软件学报&referenced_num=3&reference_num=34