计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2010年
9期
151-156
,共6页
构件%交互行为%形式化描述%自动机
構件%交互行為%形式化描述%自動機
구건%교호행위%형식화묘술%자동궤
采用形式化方法对复杂实时构件系统交互行为进行描述和验证,对于提高系统的正确性、可靠性等可信性质具有重要意义.分析了基于进程代数和自动机的构件交互行为形式化建模方法各自的优缺点,在此基础上提出了基于时间构件交互自动机的建模方法,给出了时间构件交互自动机的相关定义、组合和验证算法.时间构件交互自动机引入了时间限制、时间代价、时间代价计算半环、构件组合层次等概念,既能够描述构件交互情况,又能够清楚地表示出构件系统的体系结构信息和实时信息,便于对系统进行描述和验证.最后,结合具体应用给出了应用示例.
採用形式化方法對複雜實時構件繫統交互行為進行描述和驗證,對于提高繫統的正確性、可靠性等可信性質具有重要意義.分析瞭基于進程代數和自動機的構件交互行為形式化建模方法各自的優缺點,在此基礎上提齣瞭基于時間構件交互自動機的建模方法,給齣瞭時間構件交互自動機的相關定義、組閤和驗證算法.時間構件交互自動機引入瞭時間限製、時間代價、時間代價計算半環、構件組閤層次等概唸,既能夠描述構件交互情況,又能夠清楚地錶示齣構件繫統的體繫結構信息和實時信息,便于對繫統進行描述和驗證.最後,結閤具體應用給齣瞭應用示例.
채용형식화방법대복잡실시구건계통교호행위진행묘술화험증,대우제고계통적정학성、가고성등가신성질구유중요의의.분석료기우진정대수화자동궤적구건교호행위형식화건모방법각자적우결점,재차기출상제출료기우시간구건교호자동궤적건모방법,급출료시간구건교호자동궤적상관정의、조합화험증산법.시간구건교호자동궤인입료시간한제、시간대개、시간대개계산반배、구건조합층차등개념,기능구묘술구건교호정황,우능구청초지표시출구건계통적체계결구신식화실시신식,편우대계통진행묘술화험증.최후,결합구체응용급출료응용시례.
