Static analysis may cause state space explosion problem. In this paper we demonstrate how ordinary differential equations can be used to check the deadlocks and boundedness of the programs. We hope that our method can...
详细信息
Web navigation model provides a dynamic view for web modelling. It is useful for clarifying requirements and specifying implementation behaviors of systems from design intensions. In this paper, we propose a formal mo...
详细信息
Web service composition is a distributed model to construct new web service on top of existing primitive or other composite web services. However, current service technologies, including proposed composition languages...
详细信息
ISBN:
(纸本)9780769537580
Web service composition is a distributed model to construct new web service on top of existing primitive or other composite web services. However, current service technologies, including proposed composition languages, do not address the reliability of web service composition. Thus it is hard to predict the system reliability. In this paper, we propose a method to compute system reliability based on Service Component Architecture(SCA). We first present a formal service component signature model with respect to the specification of the SCA assembly model, and then propose a language-independent dynamic behaviour model for specifying the interface behaviour of the service component by port activities. Then the failure behaviors of ports are defined through the Enhanced Non-Homogeneous Poisson Process(ENHPP). Based on the semantics of ports, several rules have been generated to compute reliabilities of port expressions, thus the overall system reliability can be automatically computed.
Use cases have been used to describe functional requirements of information systems in a natural language. In the design phase, use cases can be used to construct design model and then the model can be checked by some...
详细信息
In this paper, we focus on the matching of parameter type and order for integration testing. From the unit testing, we can obtain two outputs: l)Interface Net that describes ports to receive parameters and to send par...
详细信息
ISBN:
(纸本)9780769537580
In this paper, we focus on the matching of parameter type and order for integration testing. From the unit testing, we can obtain two outputs: l)Interface Net that describes ports to receive parameters and to send parameters;2) Mapping Table that describes the mappings between parameters coming in and parameters going out. To analyze the Interface Net and mappings precisely, we propose a forward slicing technique with symbolic execution to obtain the dependency relation for inputs and outputs. The Interface Net together with Mapping Table will create a Directed Graph, which can be used to generate integration test cases and to check parameter type. Furthermore, a formula is given to calculate the number of test cases. At the same time, the concept called Complexity Degree, is introduced to describe how hard the test going to be.
This paper presents a port based language to describe components and component composition. This language aims to check component composition in three aspects: signature constraints, behaviour compatibility and run ti...
详细信息
ISBN:
(纸本)9781424459124
This paper presents a port based language to describe components and component composition. This language aims to check component composition in three aspects: signature constraints, behaviour compatibility and run time errors. For the run time errors, we have a result that can check if the system is in deadlock state.
Assuring the consistency between collaborative services is a challenge problem in service oriented architecture. In this paper, we propose an approach to verifying the consistency of collaborative services based upon ...
详细信息
ISBN:
(纸本)9781424445257
Assuring the consistency between collaborative services is a challenge problem in service oriented architecture. In this paper, we propose an approach to verifying the consistency of collaborative services based upon model checking. We first introduce an Extended UML Sequence Diagram for modeling dynamic behavior of collaborative service combining with UML State Chart Diagram. And then we define Collaboration-Contracts and obtain the verification model from the dynamic behavior models. Finally, wean automatically verify the consistency of collaborative services in behavior models by using an integrated SPIN-binding modeling tool Trustable MDA we developed to, In addition, a user-friendly service simulator is provided to locate the position of inconsistency.
Test data generation is one of the important tasks dur ing software testing. This paper proposes an approach to generating test cases automatically for the unit test of C programs with derived types including pointers...
详细信息
Test data generation is one of the important tasks dur ing software testing. This paper proposes an approach to generating test cases automatically for the unit test of C programs with derived types including pointers, structures and arrays. Our approach combines symbolic execution and concrete execution. The approach captures operations on variables precisely by concrete execution, and thus it is capable of handling derived types. Benefited from symbolic execution, accessing variables as array index can be solved by a substitution strategy. The substitution strategy also translates a path constraint involving variables of derived type to the one containing only primitive variables. An implementation of this approach is integrated into our test case generation tool called CAUT. Experimental results show that our approach is effective to generate test data for derived types.
A framework for modeling, analyzing and synthesizing nuclear safeguards information with various uncertainties is proposed by using a newly developed belief rule-base inference methodology (RIMER). After a hierarchica...
详细信息
A framework for modeling, analyzing and synthesizing nuclear safeguards information with various uncertainties is proposed by using a newly developed belief rule-base inference methodology (RIMER). After a hierarchical analysis of States' nuclear activities on the basis of the International Atomic Energy Agency (IAEA) physical model, the multi-layer structure of the evaluation model for States' nuclear activities is outlined. The special emphasis is given to the synthesis and evaluation analysis of the physical model indicator information by RIMER, which handles hybrid uncertain information in nuclear safeguards evaluation process. The proposed framework illustrates and clarifies the inference and synthesis formalism from a case study of nuclear safeguards information evaluation.
Service Component Architecture (SCA) provides a language-independent way to define and compose service component. The SCA assembly model should be reliable. This target can be reached by translating a formal signature...
详细信息
Service Component Architecture (SCA) provides a language-independent way to define and compose service component. The SCA assembly model should be reliable. This target can be reached by translating a formal signature model and behavior model for SCA to Promela, and Promela specifications are then verified with the model checker SPIN. SCA complements some service composition languages (such as BPEL) for enabling the more convenient and efficient service-based development. Based on our method and by using IBM WID tool, we show how to build a reliable BPEL process.
暂无评论