A program mode is a regular trajectory of the execution of a program that is determined by the values of its input variables. By exploiting program modes, we may make worst-case execution time (WCET) analysis more precise. This paper presents a novel method to automatically find program modes and calculate the WCET estimates of programs. First, the modes of a program will be identified automatically by mode-relevant program slicing, and the precondition will be calculated for each mode using a path-wise test data generation method. Then, for each feasible mode, we show how to calculate its WCET estimate for modern reduced instruction set computer (RISC) processors with caches and pipelines and for traditional complex instruction set computer (CISC) processors. We also present a method to obtain the symbolic expression for each mode for CISC processors. The experimental results show the effectiveness of the method.

With the spread of the Internet and software evolution in complex intensive systems, software architecture often need be reconfigured during runtime to adapt variable environments and design objectives. To deal with reconfigurable software architectures, the formal method should be presented to describe software architectures and express their changes so that these changes on the evolutions of software architectures could be reasoned about. However, current formal methods for reconfigurable software architectures are difficult to represent hierarchy and model context-aware systems. In this paper, we use and extend bigraph as a formal method to describe reconfigurable software architecture. By providing graphic elements and term languages, extended bigraphs can survey static and dynamic architectures easily. Then we represent basic architectural operations based on extended bigraphs, through a case describe reconfigurations with constraints and context-aware information by reaction rules, and illustrate how to check the properties to satisfy design requirements by BiLog.

UML dynamic models are important for software analysis and design. Verifying UML dynamic models to find design errors earlier is a key issue for ensuring software quality. Because of the characteristics such as concurrency and hierarchy, model checking of UML Statecharts and collaboration diagrams faces the problem of state explosion. In this paper, UML Statecharts is firstly structurally expressed by hierarchical automata and its semantics for open systems is introduced. Then, the synchronization composition of objects in UML collaboration diagrams is expatiated, based on which the global system behaviors can be constructed. Based on hierarchical automata and simulation relation between semantics structures, the compositional rules for verifying concurrent object systems are proposed. It makes possible that the construction of global state space will be unnecessary in model checking of UML collaboration diagrams. The hierarchical structures of UML Statecharts are also brought into the compositional verification, which makes the model checking of implementation models can be carried out through replacing detailed components by abstract specifications.

With the spread of the Internet and software evolution in complex intensive systems, software architecture often need be reconfigured during run time in dynamic, heterogeneous environments in order to satisfy design objectives, which poses new problems such as, does the architecture of a system conform to the given architectural style? Existing formal methods for the conformance check are either obscure to be understood, or inadequate to express parameters, global conditions, and so on. In this paper, we present an approach to check architectural instance conforming to its style based on bigraphical reactive systems (BRSs). We extend bigraph and Sigma-sorted BRS to describe architectural instance and architectural style respectively, and provide an approach to support the conformance check. The approach not only provides a visual and formal mechanism to specify architectural instances and styles, but also enriches the capability to model evolving systems and deal with parametric reaction rules, which are excellent over other existing formal methods naturally. An important theorem the changing bigraphs always preserve the constraints defined by Sigma-sorted BRS if the initial bigraph and reaction rules do is proved and a conformance algorithm is presented. Two cases are studied in order to illustrate the effectiveness of our approach.

The verification of Web services becomes a challenge in software verification. This paper presents a framework for verification of Web service interfaces at various abstraction levels. Its foundation is the interface theory for Web services, in which transaction features are incorporated. Within the framework, one may check non mutual invocation, compatibility and refinement of Web services at signature, conversation and protocol levels. At protocol level, we present a model checking approach to verifying the protocol properties in action set computation tree logic (ASCTL). The paper also discusses the integration of our framework into the Web service development

This paper presents a new approach to generating configuration-oriented executable symbolic test sequences from Extended Finite State Machine (EFSM) models. The information about the values of the context variables and the domain intervals of the input parameters are exploited to guide the derivation of the test sequences. Meanwhile, the transition guards along the test sequences are continually used to reduce the domain intervals of the input parameters. Experiments indicate that this method significantly reduces the EFSM state space to be explored and the number of non-executable symbolic test sequences to be generated. Since parameterized input events are allowed to occur in EFSM cycles, this method is suitable for testing the open reactive systems that interact with the environments via parameterized input events.

Test oracles are widely used to verify whether a system under test is running as desired. Since the correctness of real-time systems depends on the logical results of the computation and the time when results are produced at the same time, an optimized model checking-based method for test oracles generation is proposed to check if the system traces satisfy their real-time specifications at run time. Inspired by the idea of real-time model checking, the test oracles can be automatically generated from their specifications in the real-time logic MITL/sub [o,d]/ in a simpler way and modelled by a variant of the timed automata. Assertions are chosen to acquire the traces of real-time systems. A case study is presented to demonstrate the usefulness of the method proposed in this paper.

A distributed simulation environment of fluid flow as a study case is firstly brought forward and then a simulation-based universal distributed solving process that is universal in many problem domains is put forward. Based on the process, the agent-oriented early requirement analysis of the study case has been carried out basically, and the feasibility and rationality of agent-oriented method and difficulty of object-oriented method for modeling complicated intentional feature have also been discussed.

Although statecharts has gained widespread use as a formalism for modeling reactive real-time systems, testing these systems still confronts some difficulties, of which a major one is the existence of numerous and complex system behaviors. It is extremely difficult to conduct comprehensive and in-depth testing of such real-time systems. This paper presents an approach to property-oriented real-time testing. Necessary real-time extensions are proposed such that the time-enriched statecharts can describe nontrivial timing constraints. The properties to be tested are characterized by a restricted real-time logic. Then the targeted test sequences are derived from the real-time models according to the user-specified properties. Using this approach, testing efforts can be focused on particular properties of the real-time systems and usually only a small portion of the total behaviors needs to be tested.

Multiagent systems (MAS) are typical distributed systems. It is an open problem for generating test oracles for MAS. A role-based MAS model is proposed, together with some basic definitions on soft gene, role and agent. A method to generate test oracle for such a MAS is brought forward, which may address the checking of dynamic binding between agents and roles. RoboCup simulation football team case is studied to illustrate the new MAS model and the corresponding test oracle generating method.

Unified Modeling Language (UML) has been widely used in software development. Verifying if an UML model meets the required properties has become a key issue. Model checking is an important technology of automatic formal verification to ensure the correctness of design specifications. An approach of model checking UML statecharts is given in this paper At first, the brief syntax and semantics of UML statecharts are described. Then, the way of how UML statecharts is structurally expressed by extended hierarchical automaton and the labeled transition system are defined. The correctness of operational semantics of UML statecharts can be ensured through finding the maximal non-conflict transition set. For the system with infinite runs, the operational semantics can be mapped to a Buchi automaton and linear temporal logic properties of the system can be verified based on the automata theory of model checking. The paper also presents the method of verifying complex system consist of multiple objects modeled by statecharts and collaboration diagram.

Automatic generation of test data for a given path in a program is an elementary problem in software testing, the difficulty of which lies in how to solve the nonlinear constraint. Gupta et al. (1998) proposed a method, which is referred to as the iterative relaxation method, to address the above problem by linearizing the predicate functions. This paper improves the iterative relaxation method by omitting the constructions of predicate slice and input dependency set, and proves the equivalence of systems of constraints generated by both methods. Since it is not necessary for our method to analyze the dependencies between statements on the path in the course of deriving a system of constraints, our method still works when some statements are only object or executable codes rather than source codes on the path. Therefore, our method can also be used for generating test data for black-box testing and regression testing. We have developed a prototype of a path-wise test data generator whose fundamental algorithm is presented in this paper. The initial experiments with this prototype have shown that our method is practical.