High quality software requirement specification is crucial for a software development. Although much efforts and research works have been done to address the problem, the errors in user requirement are still prevent u...High quality software requirement specification is crucial for a software development. Although much efforts and research works have been done to address the problem, the errors in user requirement are still prevent us from developing high quality software. To address the problem, this paper proposes integrating graphical specification technique UML with formal specification technique to construct user requirement specification. We also present a prototype tool to perform the automatic translation from UML specification into Object-Z specification.展开更多
Model driven architecture(MDA) is an evolutionary step in software development.Model transformation forms a key part of MDA.The transformation from computation independent model(CIM) to platform independent model(PIM)...Model driven architecture(MDA) is an evolutionary step in software development.Model transformation forms a key part of MDA.The transformation from computation independent model(CIM) to platform independent model(PIM) is the first step of the transformation.This paper proposes an approach for this transformation with pattern.In this approach, we take advantage of"reuse"from various standpoints.Feature model is used to describe the requirement of the application.This can help us bring"reuse"into effect at requirement level.Moreover we use pattern to transform CIM to PIM.This can help us bring"reuse"into effect at development level.Meanwhile, pattern was divided into four hierarchies.Different hierarchies of pattern are used to help us utilize reuse at different phase of development.From another standpoint, feature model describes the problem of a domain while pattern describe the problem across domains.This can help us reuse the element in and across domains.Finally, the detailed process of the transformation is given.展开更多
Model checking techniques have been widely used in verifying web service compositions to ensure the trustworthi- ness. However, little research has focused on testing web services. Based on the research of model check...Model checking techniques have been widely used in verifying web service compositions to ensure the trustworthi- ness. However, little research has focused on testing web services. Based on the research of model checking techniques~ we propose a model checking based approach for testing web service composition which is described by using the web services choreography description language （WS-CDL）. According to worldwide web consortium （W3C） candidate recommendation, the WS-CDL specification provides a language for characterizing interactions between distinct web services using XML. Since the behaviors of web service composition are asynchronous, distributed, low-coupled and platform independent, we employ the guarded automata （GA） model for specifying the composition described in WS-CDL and using the simple promela interpreter （SPIN） model checker for detecting the collaborations of web services. Test cases can be transformed from counterexamples generated by SPIN using adequacy criteria. In this paper we apply the transition coverage criterion for generating counterex- amples. To illustrate our approach, we set ＂E-commerce service system＂ as an example for demonstrating how test cases can be generated using SPIN for compositions specified in WS-CDL.展开更多
文摘High quality software requirement specification is crucial for a software development. Although much efforts and research works have been done to address the problem, the errors in user requirement are still prevent us from developing high quality software. To address the problem, this paper proposes integrating graphical specification technique UML with formal specification technique to construct user requirement specification. We also present a prototype tool to perform the automatic translation from UML specification into Object-Z specification.
基金supported by the National Natural Science Foundation of China (Grant No.601730301)the National BasicResearch Program of China (973 Program) (Grant No.2002CB312001)
文摘Model driven architecture(MDA) is an evolutionary step in software development.Model transformation forms a key part of MDA.The transformation from computation independent model(CIM) to platform independent model(PIM) is the first step of the transformation.This paper proposes an approach for this transformation with pattern.In this approach, we take advantage of"reuse"from various standpoints.Feature model is used to describe the requirement of the application.This can help us bring"reuse"into effect at requirement level.Moreover we use pattern to transform CIM to PIM.This can help us bring"reuse"into effect at development level.Meanwhile, pattern was divided into four hierarchies.Different hierarchies of pattern are used to help us utilize reuse at different phase of development.From another standpoint, feature model describes the problem of a domain while pattern describe the problem across domains.This can help us reuse the element in and across domains.Finally, the detailed process of the transformation is given.
基金Project supported by the Open Foundation of State Key Laboratory of Software Engineering(Grant No.SKLSE20080712)the National Natural Science Foundation of China(Grant No.60970007)+2 种基金the National Basic Research Program of China(Grant No.2007CB310800)the Shanghai Leading Academic Discipline Project(Grant No.J50103)the Science and Technology Commission of Shanghai Municipality(Grant No.09DZ2272600)
文摘Model checking techniques have been widely used in verifying web service compositions to ensure the trustworthi- ness. However, little research has focused on testing web services. Based on the research of model checking techniques~ we propose a model checking based approach for testing web service composition which is described by using the web services choreography description language （WS-CDL）. According to worldwide web consortium （W3C） candidate recommendation, the WS-CDL specification provides a language for characterizing interactions between distinct web services using XML. Since the behaviors of web service composition are asynchronous, distributed, low-coupled and platform independent, we employ the guarded automata （GA） model for specifying the composition described in WS-CDL and using the simple promela interpreter （SPIN） model checker for detecting the collaborations of web services. Test cases can be transformed from counterexamples generated by SPIN using adequacy criteria. In this paper we apply the transition coverage criterion for generating counterex- amples. To illustrate our approach, we set ＂E-commerce service system＂ as an example for demonstrating how test cases can be generated using SPIN for compositions specified in WS-CDL.
