软件体系结构环境中的行为规范说明与验证

Behavioral Specification and Verification in a Software Architecture Environment

以实时线性时态逻辑作为逻辑框架，以时控自动机作为计算模型，扩展了软件体 系结构环境Armani的行为规范说明与验证的能力。从而可以在体系结构描述的基础上从结构 和行为两方面分析验证系统在体系结构层次上的重要性质，减少软件开发的风险；并且支持 非完全规范说明，具有半形式化验证与组合验证的灵活性。

This paper extends the software architecture environment Armani wit h the ability of behavioral specification and verification in a real-time linear temporal logic framework using timed automata as computing models. It can help to ensure certain essential archiectural properties both from structural and fu nctional aspects and thus owns the potential to reduce the software development risk before the development process proceeds to implementation phase. The propo sed extension allows incomplete specification and supports semi-formal and compo sitional verfication.