Chinese Journal of Computers   Full Text
Title	An Integrated Verification Model atsFPM Based on Functional,Time and Spatial Constraints
Authors	NIU Jun1),2),3) ZENG Guo-Sun1),2) CHEN Bo1),2)
Address	1)(Department of Computer Science and Technology, Tongji University, Shanghai 201804) 2)(Key Laboratory of Embedded System and Service Computing of Ministry of Education, Shanghai 201804) 3)(College of Information Engineering, Zhejiang Business Technology Institute, Ningbo, Zhejiang 315012)
Year	2009
Issue	No.4(740—750)
Abstract &   Background	Abstract 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. Keywords function and performance; spatial constraint; integrated verification; secure and trusted Background This work is supported by the National Natural Science Foundation of China under grant Nos.90718015 and 60673157 and the National High Technology Research and Development Program (863 Program) of China under grant No.2007AA01Z425, and the National Basic Research Program(973 Program) of China under grant No.2007CB316502. An important object of these projects is to investigate how to analyze and verify the complicated information system such as internet software or embedded system by model checking approaches automatically, and come to a conclusion whether the system is secure, dependable and trustworthy. Our main task is focused on analysising information system’s function and performance by some formal models such as labeled transition systems or continuous time Markov chains and some model checking algorithms.The function model is based on labeled transtion systems and performance is based on continuous time Markov chains or continuous reward model. The traditional work on the security analysis of complicated information system’s is mainly focused on functional analysis by LTL, CTL or CTL* model checking approaches.Some approaches by which we can pursuing performance analysis on time or space have been existed. The time properties are described by adding time parameters on transition labels and the spatial properties are described by adding the information which express the constraints of spatial resource such as time,memory and cost.The research group proposed several verification approaches about the web service’s security by the analysis of their behavior chains patterns. With lack of a combinatorial model and verification approaches on function and performance at one time,this paper first introduces a integrated verification model atsFPM,which integrates the continuous time Markov chains and continuous reward model and includes functional,time and spatial constraints,and then proposes a model checking algorithm by extends the continuous stochastic logic and continuous stochastic reward logic.The results shows that the atsFPM and the model checking approaches woule be helpful to somebody while evaluating security.