Behavioral Specification and Verification in a Software Architecture Environment
Xiaoli Zhi · Jisuanji gongcheng · 2003
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.