Integrated verification model atsFPM based on functional, time and spatial constraints

作     者：Niu, Jun Zeng, Guo-Sun Chen, Bo 

作者机构：Department of Computer Science and Technology Tongji University Shanghai 201804 China Key Laboratory of Embedded System and Service Computing of Ministry of Education Shanghai 201804 China College of Information Engineering Zhejiang Business Technology Institute Ningbo 315012 China 

出 版 物：《Jisuanji Xuebao/Chinese Journal of Computers》 (Jisuanji Xuebao)

年 卷 期：2009年第32卷第4期

页      面：740-750页

核心收录：

学科分类：1205[管理学-图书情报与档案管理] 08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：Information systems 

摘      要：Nowadays complex information system s integrated formal models of function verification and performance evaluation lack properties constraint about space aspect. This paper presents an integrated verification model atsFPM by defining a space requirement function over the states of the considered information system. The patterns of paths which are based on regular expressions is proposed in order to specify the functional specifications. The syntax and semantic of the model atsFPM is defined. A conversion product model is obtained by the combination of the system model and the automaton of the pattern of paths which expresses the functional specifications. The verification of the model atsFPM is tackled by the performance verification technique of Markov Reward Model. Experimental results show that the atsFPM model and its verification approach can satisfy the modeling of information system and verification of functional and performance specifications.