A Software Behavior Oriented Requirements Model and Properties Verification

Requirements model and its verification are important procedures in software requirements. In this paper, the existing methods on requirements model are discussed and the related works of software behavior are concerned; furthermore, why utilizing software behavior in requirements model is illuminated. So a software behavior oriented requirements model is proposed formally which is named behavior description language (BDL). Its syntax and semantics of the model are given subsequently, and the hierarchy of behavior-oriented requirements model is presented based on BDL. In order to compare BDL with the current results and make full use of the latter related tools, the transformational relation is considered between BDL and CCS (calculus of communication system) which is an algebra process developed by Milner Robin. A transformation function which maps BDL into CCS is constructed and denoted by M. For the sake of verifying properties of behavior-oriented requirements model, consistency of system, safety of system, behavioral trust and behavioral non-termination are depicted by μ-calculus, which is used to describe properties of labeled transition systems and for verifying these properties. At the end, an example described by BDL is analyzed and the specified properties are verified through CWB (Concurrency WorkBench) which is a model checking tool of CCS.