%0 Journal Article
%T 面向嵌入式实时软件的需求规约语言及检测方法
%A 舒风笛？
%A 毋国庆？
%A 李明树？
%J 软件学报
%P 1595-1606
%D 2004
%X 针对嵌入式实时软件需求规约及其检测问题,提出了基于层次并发有穷状态机的可合成的图形化建模语言rtrsm*(real-timerequirementsspecificationmodel*),利用转换有效期和事件预定机制来描述时间限制,能够较好地支持系统交互性和实时性的建模.为弥补rtrsm*作为操作性规约语言不便于性质描述的问题,提出了命题时序逻辑ritl(real-timeintervaltemporallogic).该语言以时间状态序列为语义模型,具有基于区间和时间点的量化时间属性描述功能,能自然、全面地描述rtrsm*模型性质.介绍并讨论了基于两种语言的规约检测方法和技术,主要包括系统状态空间有穷的rtrsm*模型状态可达图的相关问题和规约的模拟执行.
%K 嵌入式实时软件
%K 需求规约语言
%K 需求规约检测
%K 可达图
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=20041102&flag=1