Traditional software defect localization aims to locate defective files, methods, or code lines based on symptoms such as defect reports. In comparison, Just-In-Time (JIT) software defect localization focuses on identifying defective code lines when a defective code change is initially submitted. It can identify issues at the code line level before the defect becomes apparent, preventing it from adversely affecting the software. Although researchers have proposed various methods for JIT defect localization, existing methods still have the following shortcomings: (1) Most methods rely heavily on tokens from single code lines to calculate naturalness for defect localization, which makes it challenging to effectively distinguish between code lines that have the same content but different labels (defective code lines or non-defective code lines) - termed Duplicate Lines with Different Labels (DLDL). (2) Existing methods represent code in the form of sequences, neglecting the structural information of the code. Therefore, we propose a JIT defect localization method based on code graph representation. First, we construct code linelevel code graphs for code changes to distinguish DLDL explicitly. Next, to extract sequential and structural information from the code, we propose a code graph representation model with contrastive learning to generate graph feature vectors and node scores with rich semantics. Finally, we calculate the naturalness of code lines based on the graph feature vectors and node scores. Using this naturalness, we identify defective code lines. Experimental results show that our JIT defect localization method outperforms the state-of-the-art methods.

Formal methods have been widely used to support software testing to guarantee correctness and reliability. For example, model checking technology attempts to ensure that the verification property of a specific formal model is satisfactory for discovering bugs or abnormal behavior from the perspective of temporal logic. However, because automatic approaches are lacking, a software developer/tester must manually specify verification properties. A generative adversarial network (GAN) learns features from input training data and outputs new data with similar or coincident features. GANs have been successfully used in the image processing and text processing fields and achieved interesting and automatic results. Inspired by the power of GANs, in this article, we propose a GAN-based automatic property generation (GAPG) approach to generate verification properties supporting model checking. First, the verification properties in the form of computational tree logic (CTL) are encoded and used as input to the GAN. Second, we introduce regular expressions as grammar rules to check the correctness of the generated properties. These rules work to detect and filter meaningless properties that occur because the GAN learning process is uncontrollable and may generate unsuitable properties in real applications. Third, the learning network is further trained by using labeled information associated with the input properties. These are intended to guide the training process to generate additional new properties, particularly those that map to corresponding formal models. Finally, a series of comprehensive experiments demonstrate that the proposed GAPG method can obtain new verification properties from two aspects: (1) using only CTL formulas and (2) using CTL formulas combined with Kripke structures.

Model-based testing has been highlighted in the last few decades. Many improvements have been proposed for this testing method. One improvement is the use of extended regular expressions (EREs) for modeling software behavior, and then using the ERE model to generate test paths. To improve the theory of test generation based on the ERE model, this article presents an algebraic system, named transition algebra, by extending Kleene algebra. Eight operations and their corresponding operational properties, including basic and nonbasic operational properties, are designed for transition algebra, and all such properties are proven. Five examples are given to illustrate the use of ERE modeling and algebraic operations. To ensure the automatic generation of test paths from the ERE model, the article proves that any ERE model constructed by transition algebra can be converted to a set of transition sequences. Compared to Kleene algebra with tests, transition algebra has more operations to build a powerful ERE model and more operational properties to process the ERE model for the generation of test paths.

Service-based systems are a new software mode for distributed business processes integration. It is difficult for traditional testing methods to verify the functional and nonfunctional requirements of software. To address this problem, this paper proposes a visual verification platform to quantitatively compute the reliability and cost for evaluating the performance of service-based systems in the design phase. First, an extended automata model namely Probabilistic Reward Labeled Transition System (PRLTS) is proposed to formalize both the functional behaviors and nonfunctional features. Then, the formal language of probabilistic model checker PRISM is introduced to show the grammar of the target verification codes that we want to transform. Second, XML description tags of Business Process Execution Language (BPEL) is parsed to generate the functional behaviors using different kinds of transformation rules, based on which the probability matrix and reward concept are employed to denote the service’s reliability and cost, respectively. Third, the PRLTS model is turned into the input language of PRISM, where the graphic description language DOT of Graphviz is used as an intermediary to display system behaviors in a visual way. The model layout allows the designer to manually adjust the behaviors of the PRLTS model, where verification codes can be dynamically updated according to the changes in modified information. Fourth, to perform quantitative verification, the verification property in the form of the Probabilistic Computation Tree Logic (PCTL) formula can be automatically generated when the requirement model of the service-based system is inputted, during which the threshold value of qualitative property will be initially computed and returned as a recommended value. This allows the user to modify the qualitative property in an interactive way. Furthermore, experimental analysis of the real-world case study demonstrates the feasibility of the proposed method. Thus, our platform provides guidance for quantitative verification and graphical visualization for effectively generating formal models and checking the quantitative properties for service-based systems.

Wireless communication protocols are indispensable in Internet of Things (IoT), which refer to rules and conventions that must be followed by both entities to complete wireless communication or service. Wireless protocol conformance testing concerns an effective way to judge whether a wireless protocol is carried out as expected. Starting from existing test sequence generation methods in conformance testing, an improved method based on overlapping by invertibility and multiple unique input/output (UIO) sequences is proposed in this paper. The method is accomplished in two steps: first, maximum-length invertibility-dependent overlapping sequences (IDOSs) are constructed, then a minimum-length rural postman tour covering the just constructed set of maximum-length IDOSs is generated and a test sequence is extracted from the tour. The soundness and effectiveness of the method are analyzed. Theory and experiment show that desirable test sequences can be yielded by the proposed method to reveal violations of wireless communication protocols in IoT.

Using Clustering algorithm to improve the effectiveness of test case prioritization has been well recognized by many researchers. Software fault prediction has been one of the active parts of software engineering, but to date, there are few test cases prioritization technique using fault prediction. We conjecture that if the code has a fault-proneness, the test cases covering the code will find fault with higher probability. In addition, most of the existing test cases prioritization techniques using clustering algorithm don't consider the number of clusters. Thus, in this paper, we design a test case prioritization based on clustering approach combining fault prediction. We consider the method to obtain the best number of clusters and the clustering prioritization based on the results of fault prediction. To investigate the effectiveness of our approach, we perform an empirical study using an object which contains test cases and faults. The experiment results indicate that our techniques can improve the effectiveness of test case prioritization.

This paper proposes an approach to evaluate the reliability of cloud rendering system. After the requirement analysis, the rendering system was divided into three modules: preparing files, requesting resources, and rendering task execution. Each module may have an exception that will reduce reliability, and has the ability to recover it. To expose these details, the discrete-time Markov chain (DTMC) is improved to formalize the cloud rendering system. The model contains an abnormal state set representing exceptions and errors such as file corruption and failure to rendering subtasks. Then, a series of formal properties are defined to describe reliability in detail. The proposed method gives full consideration to the processes of rendering tasks. Finally, the properties are verified by performing PRISM in a quantitative way. The experiment shows that our method is effective to evaluate the reliability of the cloud rendering system.

Web services bring more conveniences for users and developers. However, it makes user face the problem of service information explosion. The personalized service recommendation solves the problem. This paper proposes a method to predicting the system reliability which bases on user context information in mobile computing environment. The method construct user behavior model by formatting user location context and then quantitative verification is performed to estimating whether the recommended service meet the requirements of users. Finally, experiments are carried out to demonstrate the effectiveness of our method.

Security protocols are the key to ensure network security. In the context of the state of the art, so many methods have been developed to analyze the security properties of security protocols, such as Ban logic, theorem proving and model checking etc. This paper used model checking method to formally verify security protocols because of its high degree of automation, briefness and effectiveness. The model checker Spin with sound algorithm design has an extraordinary ability of checking and a good support for LTL. This paper studied the use of Spin on security protocols, and proposed a more effective intruder model to formally verify the security properties of security protocols, such as authentication. The method in this paper decreased the number of model states by a wide margin, and avoided the state space explosion effectively. This paper exampled NSPK protocol and DS protocol, and good experimental results were shown.

Service-Oriented Computing (SOC) and Service-Oriented Architecture (SOA) provide a paradigm for creating composite service with distributed web services over the Internet. Through the integration and coordination of distributed web Services, Web Service Business Process Execution Language (BPEL) can deploy a composite service rapidly. However, in a complex dynamic network environment, it is difficult to guarantee the reliability of BPEL application. To verify the reliability of the BPEL process, this paper proposes a method which can extract the model from a BPEL process and analyze it through probabilistic model checking with Prism model checker. During the extension process, we add reliability attribute to each invoked sub-services. By structure extraction, the BPEL process is transformed to a PLTS system. Then, we generate a suitable analysis Markov model according to the feature of the PLTS model. Finally, we use PCTL formula to describe the properties of the system, and check it with Prism tool.

We present a formal specification to engineer situated multi-agent Systems (situated MAS), which has revealed the need for specifying and reasoning of its global property. This paper shows how MAS is specified with modified Object-Z notation with trace semantic of action system, and how to reason about safety and liveness property in this specification. Independent and joint MAS examples are are used to illustrate specifying and reasoning in specification for situated MAS.

Widely applied and quickly developed as the SOA theory has been, the instability of distributed Web services will lead to services composition failure. Currently, a hot research topic is that when does the system can make an appropriate adjustment of the system structure dynamically to ensure the system runs at the best performance while the runtime environment or requirement is changed. To address this problem, this paper proposes an approach to predicting the system survivability which bases on log statistic. The method gets the system usage model by monitoring Web log files, and then constructs value model and adopts quantitative model checking to forecast the system survivability to estimate whether the system is survivable in a certain period of time.

Graphical User Interface (GUI) provides a popular and convenient way for the user to freely interact with the systems which makes it widely used in various software applications, it has become an important and indispensable part of today's software. Owing to the characteristics of GUIs different from the traditional software, traditional test techniques and methods cannot satisfy the requirements of GUI testing. Modeling and testing of GUIs-based system is a difficult and challenging work. GUIs-based application is an event-driven application. In GUIs, there exist not only the input events and output events, but also the internal events. In this paper, we identify the input events, output events and internal events and propose an approach to modeling and testing of GUIs-based system using the IOLTS, and input events, output events and internal events are also taken into account. Constraints on events and regular expressions on validation of data are given out. The interactions of GUIs are constructed by the corresponding output events. Finally, tests generation and tests instantiation are given out.

Service software deployed in E-commerce and finance fields needs working under 7*24 houses mode. If any failure occurs, service reconfiguration should be immediately executed to find appropriate services from candidates in order to guarantee the availability of core business. Thus, service software cries for an effective approach to constantly adjust its form for responding to varying user requirements and instable runtime environments. To this end, this paper proposes a probabilistic model checking-based Web service reconfiguration architecture. First, it proposes a predictive Web service monitoring approach based on probabilistic model checking. Second, it gives a Web service dynamic service selection approach which takes compatibility checking into account. The single-source service selection works to execute service replacement, while the multi-source service selection carries out service simulation. Third, it discusses a Web service dynamic reconfiguration verification approach where the Probabilistic Counterexample-Guided Abstraction Refinement (Probabilistic CEGAR) is introduced to alleviate the state space explosion problem.

The language of Live Sequence Chart (LSC), a multi-modal extension of MSC, introduces the distinction between mandatory and possible on the level of the whole chart and for the chart elements. While the LSC still extend the MSC qualitatively, when it comes to capturing the quantitative behaviors, the deficiency emerges. As for the probabilistic systems, i.e., systems that exhibit probabilistic aspects, probabilistic properties are considered as the most important requirements and need to be captured quantitatively. To address this, we propose a requirements description language called pLSC. Supported by the measure theory and the probability theory, the language pLSC describes the interactions quantitatively to suit the probabilistic systems from two dimensions of probabilistic branches and three-stage events. The paper introduces the graphical and textual presentation of the pLSC.

During the development process of Web application, two essential phases are software testing and code refactoring. However, automatic testing script plays an important role in test automation. It has been a hot research topic in Web application. In order to refactor the JavaScript code of Web application more conveniently, an approach to automatic script generation from the defined test case is introduced in this paper. First, it describes the test case using customized XML format. Then, since Selenium platform supports multi-browsers testing, a method to transform XML description into test scripts based on Selenium framework is proposed as the emphasis.

Building a simplified model for testing complex software system has been highlighted for optimizing test generation. This paper presents an approach to generating the constrained FSM with the scenario. Firstly, we use FSM to describe the behavior model of the target system. Then, we study the method of modeling scenarios with UML diagrams, including use case diagram, activity diagram, sequence diagram and statechart diagram. We describe how to achieve the constraint process by means of mapping and projection operations between FSM and UML diagrams. Finally, we obtain a reduced FSM by using UML activity diagrams to constrain FSM. The main contribution of the paper is to present an effective modeling method to optimize testing generation from the model.

Summary form only given: Web service has been an important solution to achieve resource sharing and application integration in the Internet era, which can develop the most promising software application with the on-demand changing computing paradigm, through service reuse and dynamic synthesis. Now, more and more enterprises and organizations have taken part in the emerging service software industry, expand their cooperation and explore enterprise solution via Web service and service composition. In this talk, I survey recent research in Service Dynamic Reconfiguration. Service-oriented software needs an effective approach to constantly adjust its architecture for responding to varying user requirements and instable runtime environments, where one of the most challenging issues is how to effectively execute a dynamic evolution for Web service and to ensure that the critical business application is trustworthy. To this end, we apply the probabilistic model checking to the implementation of Web service dynamic reconfiguration. According to the lifecycle of Web service dynamic reconfiguration, our research is partitioned into three parts including Web service monitoring, Web service dynamic reconfiguration and Web service dynamic reconfiguration verification. As a result, the verified reconfiguration will be used for handling the failed service.

Web service reconfiguration plays a critical role in Service-Oriented Software (SOS), which provides a self-adaptation technique to ensure the business-critical application can be correctly worked when an SOS system is deployed in the uncertain Internet environment. To address this problem, the primary task is to select substitution services for handling the current failure service, such as the atomic service or composite service. In this paper, the service process of Web service is initially formalized in the form of a probabilistic timed model PTWSB at both of the behavior level and QoS level. Then it gives two model-based reconfigurations with different service selection demands, mainly the single-source service reconfiguration and multi-source service reconfiguration. Our approach has a good potential application prospect in Service-Oriented Software.

A formal and incremental approach is needed to introduce new agents in the development of multi-agent system (MAS) due to its intrinsic complexity. Incremental development with refinement theory is a traditional way to guarantee the dependability of a system. We specify MAS with Object-Z notation and under trace semantic of action system, give the mathematical relation model and refinement rules of superposition refinement based on the relational model and Object-Z notation. The refinement rules provide a foundation for introducing agents in MAS. A case study of repairing robots is used to show whether agents are introduced correctly.

It is an important problem to generate test data from EFSM model in model-based testing, but it is time-wasting to generate test data for the infeasible paths, so determining the feasibility of the paths before generating test data for them is necessary. The feasibility of EFSM transition paths is analyzed by combing slicing with theorem proving. It is divided into two phases. In the first phase, the transitions related to the predicate on each transition in the path are got by backward slicing. And in the second phase, the feasibility of the path is determined by theorem proving to prove whether the post-condition of the transitions related to the predicate implying the predicate or not. Experimental result shows that the feasibility of the paths can be decided effectively and the number of theorem proving is reduced greatly, the infeasibility of the path also can be checked quicker by the proposed method.

Network, such as Internet and Intranet, has penetrated into people's daily life. Router is one of the essential equipments which take an important role in the network and form a large and complicated network. However, huge amounts of routers in the network make the network communication and data routing more complex. How to insure the reach ability and correct communication of Internet is a challenge. In this paper, an approach is proposed to formally model and verify the router-based network. Then, we employ a transition system (denotes TS) to model the router-based network, and make use of the Bisimulation-Quotient Algorithms to obtain the bisimulation quotient of the finite transition system, denoted TS/~. It could be easy to verify properties on the system TS/~. Any verification result for TS/~ carries over to TS and this applies to any formula expressed in either LTL, CTL, or CTL*. This approach can facilitate verification since verification problems are particularly space-critical. Finally, some important properties of routing such as routing reach ability, routing path length, are verified.

Effective testing can develop quality software with higher productivity at a lower cost. Redundancy in the test suite increases the execution cost and consumes scarce project resources. Due to time and resource constraints in testing, test suite reduction techniques are required to remove those redundant test cases from the test suite. Since Weighted Set Covering Techniques can be used to resolve the test suite minimization, the paper presents a novel approach, called as Modified Greedy Algorithm, based on the Weighted Set Covering Problem (WSC). The WSC is, given S, for each set s ∈S a weight ws>;0 is also specified, and the goal is to find a set cover C of minimum total weight Σs∈Cws. The research aimed to reduction of the test suite which generated by Student Achievement Retrieval Navigation Model. Through comparing with existing algorithms, our algorithm can not only produce the minimum test suite is the smallest, but also minimum the total cost.

There are many variants of Petri net at present, and some of them can model system with both function and performance specification, such as stochastic Petri net, and generalized stochastic Petri net. In order to address the issue of modeling system with probabilistic behaviors, a kind of Petri net with probability (probabilistic Petri net, PPN) is proposed in this paper. Then an action-based PCTL is developed to interpret logical semantics for PPN system. The usefulness of PPN system is illustrated by modeling and specifying an elaborate model of travel arrangements workflow.

As Web services are becoming more and more complex, there is an increasing concern about how to guarantee the correctness and safety of Web services composition. This has driven many researchers to study the performance analysis of dynamic atomic service selection, as well as functional verifications. In this paper, we focus on not only modeling the behaviors of atomic service, but also verifying the properties in a quantitative way. First, we apply probabilistic timed model checking to model and verify the behaviors of atomic service by extending interface automata, and propose a technique to formally estimate software performance which exhibits stochastic behaviors with time constrains. Second, the probabilistic timed computation tree logic (PTCTL) formulae are used to express the reliability properties. Third, a failure may occur stochastically when an invocation is triggered through interface operation. We present an internal interaction model, based on which we can dynamically pick out a highest reliable execution sequence for Web services composition. Finally, a case study is demonstrated and experimental results are discussed. In conclusion, our approach provides with an underlying guideline for Web services composition.

As Web applications evolve, their structure may be-come more and more complex. Web frameset is used to organize multiple frames and nested framesets to make the layout of some Web pages more identical and bring the development of Web applications easier, which was wildly used in today's Web applications. How to model and verify the frameset-based Web applications is a challenge. In this paper, special care on Web frameset is paid and an approach to modeling and verifying Web application's navigation with Web frameset is proposed. The Composition semantics of Web Frame-set was give out which can be used to construct complex Web Frameset. Additionally, FSM was employed to describe our models with Web Frameset. Then, we transform FSM model into Kripke structure. Finally, taking advantage of the properties which were generated, we verified our model with Web Framesets. And according to results of verification, we improve our models.

The Web service composition (WSC) has been widely used in Service-Oriented Architecture (SOA), which is an effective integration of the distributed and heterogeneous business applications. In contrast to the component-based software, dynamic reconfiguration occurs more frequently in Web services-based software for self-adapting and self-managing their computing capabilities due to the uncertainty of dynamic Internet environment. Verifying these stochastic and nondeterministic behaviors is becoming a hot topic in model checking of Web services (WSs) application engineering. Abstraction refinement technique as an effective approach to alleviating the state explosion problem is particularly suitable for verifying the complex WSC. In this paper, we extend the classical abstraction refinement technique CEGAR (Counterexample-guided abstraction refinement) to make quantitative verification of WSC applicable and efficient. To model WSC, a probabilistic service behavior model (p-SBM) is proposed in form of Markov Decision Process (MDP). To verify WSC, the abstraction is defined by means of a quotient on states with respect to some probabilistic equivalence relation. Once counterexample is produced in the abstract model, verifying whether the counterexample is real or spurious is carried out. Based on the counterexample-guided technique, an iterative abstraction refinement process is performed to progressively refine the abstract model until either there is no abstract counterexample or a valid counterexample is verified. The case studies which are discussed throughout the paper demonstrate that our approach takes advantages than the traditional approaches.

With a good understanding of mobility mechanisms of WS-CDL, we can easily design applications that acquire, during the execution, all the information they need to invoke services. One of the means to ensure good interoperability between Web services is to formalize their mobility characteristics. Process algebras, such as π-calculus can be used to formalize Web Services characteristics and ensure that they satisfy some conditions required in SOA. The notion of mobility in process calculi refers to the fact that a process is able to exchange names as values. The core of π-calculus is based on interaction, using channel names as data, and the ability to generate fresh and unique names. This paper provides the basis for reasoning on formalizing mobility characteristics of Web services choreography using the process algebra π-calculus which is, according to Robin Milner, a model of concurrent computation based on the notion of naming. Formalizing mobility helps us to understand the nature of mobility, to reason about the behavior of mobile systems, and to develop model checking tools that are used to verify system correctness.

High quality test cases can effectively detect software errors and ensure software quality. However, except the regular expression-based test generation method, test cases generated from other model-based test generation methods have not contain the whole information of the model, resulting in test inadequacy. And test cases derived from regular expression have the prohibited lengths that cause the sustainable increase of test cost. To obtain high quality test cases, we suggest a new method for test generation by way of regular expression decomposition. Unlike the previous model decomposition techniques, our method lays emphasis on information completeness after regular expression is decomposed. Based on two empirical assumptions, we propose two processes of regular expression decomposition and three decomposition rules. Then we perform a case study to demonstrate our approach. The results show that our approach generates high quality test cases as well as avoids the problem of test complexity.

This paper proposes a new model checking-based test generation approach for Web applications. The Kripke structure is reconstructed to model the Web application from the end users' perspective. Test coverage criterion is expressed as trap properties in CTL so that counterexamples can be instantiated to construct test cases. But a counterexample for each trap property is generated will result in too many redundant test cases. So, a test deduction rule and an algorithm based on the greedy heuristic are given to resolve this problem. The test sequences finally generated are those satisfy the coverage criterion and have no redundancy. Throughout the paper, a typical small case study of the WGVS (Web Grade View System) is used to illustrate our approach. This approach presented can help to generate test sequences automatically for Web application and it is a significance complement to the model checking test generation.

As Web applications evolve, their structures become more and more complex. Web browsers may influence on the correctness of the Web applications, and Web browser’s interactions can cause further complications of Web application. Existing navigation models are static ones on the whole. Users’ navigation paths are all determined on stage of model design. Web browser interactions have not been taken into account make them different from practical navigation in Web applications. Moreover, as Web applications evolve and new technologies emerge, adaptive navigation was wildly incorporated in current Web applications. It aggravates the complexity of Web navigations. In this paper, a practical approach to modeling of Web applications and generating tests was pro-posed. And special care is taken on Web browser’s interactions and adaptive navigation during the user’s traversal within hypermedia space. At last, test generation is given out which satisfy the corresponding coverage.

FSM-based testing can obviously reduce the cost of test generation. So many FSM-based test generation methods have been presented to generate effective test sequences. Most of them need to construct the characterizing set of the FSM. However, there are two disadvantages in the existing algorithm for building the characterizing set. One is that time efficiency of the algorithm is hard access to our satisfaction. Another is that the obtained characterizing set may contain some redundancies. To overcome these two disadvantages, we propose the RTMD algorithm to obtain the characterizing set from the FSM, and give four theorems to ensure the correctness and effectiveness of the RTMD algorithm. Then we perform a case study to compare the existing algorithm with the RTMD algorithm. The results show that the RTMD algorithm has shorter time-consuming than the traditional algorithm as well as obtains more effective characterizing set.

The theorem proving is the basis on Tableau method. The refinement process that transforms a specification to program regards a theorem proving process. If the proof is correct, then a program that satisfies its specification can be extracted from the proof steps. This paper proves that the program is totally correct and conforms to its specification.

The problem of redundancy among test sequences derived from different FSM-based test coverage criteria often emerges in practice, resulting in the increasing of test cost of software. To solve this problem, a novel approach by way of string matching to eliminating redundancy among test sequences is presented in the paper. Four types of redundancies of test sequences are described and the corresponding reduction rules are also designed. To ensure the effectiveness of redundancy reduction, a transformation rule to convert the ineffective test segments into the effective test sequences is proposed. And then a novel algorithm for redundancy reduction is designed and implemented with Java language. Finally an example is illustrated for the achievement of our approach. Comparing with the existing researches about redundancy reduction, our approach not only eliminates most redundancies among test sequences, but also promotes the application of FSM-based test coverage criteria in practice.

Scenarios have been shown to be very helpful for requirements elicitation. However, they only capture partial behaviors of interaction among system component instances, and system behaviors are modeled by sequences of events. Such a behavioral model only captures parallel composition without synchronization in the sense that all the sequences of events are generated in an interleaving semantics. In this paper, we introduce a time model which is a category of time domains. We provide a trajectory model for the sequence of events. A trajectory describes precisely which events occur along the points of its time domain and show that categorial products allow us to compute parallel composition of behaviors with synchronization constraints. Our approach is helpful for broadening research vision of software engineering.

As more and more services and information are made available over the Internet and Intranet, Web sites have become extraordinarily complex, while their correctness and reliability are often crucial to the success of businesses and organizations. Additionally, the behavior of the Web browsers may have impact on the correctness of the Web applications: a Web application providing all correct functionality by itself may however malfunction when it is put into its supporting environment. Consequently, the Web browserpsilas interactions should be taken into account at the stage of modeling Web applications. Software testing is a primary way of improving software reliability and assuring software quality. This paper proposed an approach to modeling Web applications by the means of combination of Web functional modules and the browserpsilas interactions. A Web application is referred to as a system which consisted of many different functional modules. At last, test generation is given out which satisfies the corresponding coverage criteria.

Web applications can only be accessed through dedicated client systems called Web browsers. Most current Web browsers offer many tools or facilities for Web page revisiting, including the back and forward buttons, refresh, favorites, link menu and history lists etc. Users can press the back or forward buttons to negatively influence the behaviors of Web application navigation. Existing navigation models are static ones on the whole. Userspsila navigation paths are all determined on stage of model design. Web browser interactions have not been taken into account make them difference from practical navigation in Web applications. Accordingly, special care is taken on Web browser interactions during the userpsilas traversal within hypermedia space. We give out the concept of safety critical region (SCR) and propose an approach to modeling on-the-fly navigation models. The Kripke structure is employed to describe the on-the-fly navigation models. Coverage criteria of Web browser inter-actions, such as, node coverage, transition coverage triggered by actions, SCR coverage, are exploited to derive the properties of Web browser interactions in CTL. Ultimately, we use SMV, the model checking tool, to verify the on-the-fly navigation models.

Service-oriented architecture (SOA) and model-driven architecture (MDA) are the hottest topics of discussion currently with regard to enterprise architecture. This paper presents an approach for transforming computer independent model (CIM) to platform independent model (PIM) separating implementation technologies and platforms from the business logic in an easy and uniform way. The approach mainly includes the following two parts. The first part gives a service-oriented way to model the requirement. The requirement model addresses software as a service model for forward looking enterprise; the second part gives a model refinement mechanism and a set of refinement rules. The refinement mechanism and rules can transform the requirement model to a set of loosely coupled services and can match these services to their suitable components and interfaces. In a word, this paper provides a uniform way to transform business requirements to their service implementation, and this transforming process can be clearly traced and analyzed.

To ensure the requested quality of Web applications as expected, it is critical and challenging to test them. This work defines Web application schema and constructs Web application relation graph in order to model Web applications. An approach to generating test paths is presented by establishing path-generating graph which is derived from the Web application relation graph and used to produce path expressions. The test paths can be easily employed to construct test cases if user input values are provided. For illustration, a case study of the SWLS (Simple Web Login System) is exemplified. Moreover, a path generation strategy is suggested in accordance with the "divide and conquer" principle when the Web application under test is complicated. The strategy makes the Web application less complex and more controllable. This also restricts the state space explosion in a sense. The test path generation approach presented is an important supplement to the existing Web application testing.

Web applications can only be accessed through dedicated client systems called Web browsers. Most current Web browsers offer many tools or facilities for Web page revisiting, including the Back and Forward buttons, Bookmarks and History lists. These tools or facilities, on the one hand, help the users find the necessary information in hypermedia space; on the other hand, however, they also confuse the users due to their specific interface design against user cognitions. In this paper, special care is taken on Web browser interactions during the user's traversal within hypermedia space in order to specify possible inconsistencies between Web browser interfaces and user cognitions. GFSMs (Guarded Finite State Machines), which are augmented FSMs are employed as a tool to model Web browser interactions. For illustration, a simple login system of a Web application is exemplified.

This paper focuses on automated verification to check whether the behavior of a Web application conforms to its design. The Object Relation Diagram as design model and the Kripke structure as implementation model are employed to describe the object structure and the external observable behavior of a Web application respectively. We propose an approach to automatically generating from the design model a collection of temporal logic properties with respect to the specified consistency criteria. Then model checking can be performed on the implementation model to verify these generated properties. A simple Web application example is used to illustrate our approach through this paper. Our prototype can automatically analyze design models to build the properties in CTL and delegates the task of property verification to the existing model checker SMV where the implementation model is typed in manually.

The capability of model checkers to construct counterexamples provides a basis for automated test generation. However, many model checking-based testing approaches just focus on generating test sets with respect to some coverage criteria. Such test sets generally are large and inefficient because of much redundancy. We propose an on-the-fly approach that performs test generation and redundancy elimination by turns. Our approach employs a test-tree to pick out and represent a subset of tests with equal coverage for a test criterion and no redundancy. Along with model checking for a property, a new test sequence is derived from the counterexample and is used to detect redundant properties, and then is winnowed by the test-tree as well. We demonstrate the approach by applying some small examples to our prototyped algorithm.

The concept of software architecture (SA) provides a new way for the transition from the construct and requirement to implementation. Software architecture style is a classification of SA. Different style has different system characteristic. Through the research of software architecture style, we can direct the software development well using SA. Formalizing software architecture style made the communication more precise and convenient at the level of SA. Formalizing software architecture style will be beneficial to formal verification and comparison of different style. This paper proposes the service oriented software architecture style, formalizes the new service oriented SA style using formal specification notation Z, gives the definition of match and composition of service component, analyses the replacement of SA style and proves four theorems of replacement

Retrieving reusable service components that satisfy the user's requirements is a difficulty in component-based software development. This paper builds a domain ontology of computer, and proposes an approach to domain ontology-based software component retrieval. Different from the approach to keyword based retrieval, this approach can refine and extend the user's initial query by query reasoning and provide fuzzy retrieval based on component similarity and relatedness. The whole approach extends the software reusable library to the World Wide Web. In the retrieval process, a user query in natural language is translated into RDF representation formats in order to augment retrieval recall and precision by deploying the same semantic representation technologies on both the user query side and the component side. We built the domain ontology using Protege2.1.

A formal specification is usable only if it is consistent or non-conflictive. In traditional programming languages, the consistency checking for program is performed at run time. But formal specifications are not executable in general. The syntax parsing and semantics checking in certain tools are not effective for the consistency checking sometimes. Hence, it is difficult to verify the consistency of a formal specification. This paper presents an approach to generating relevant proof obligations for Object-Z specification systemically. It aims to verify the consistency of a specification developed with Object-Z, which enables the specifier to gain confidence. Because Object-Z is an object-oriented formal specification language and has inheritance characteristic, we discuss it from several aspects and take into account the reuse of proof obligation emphatically. Finally, we make use of the theorem prover Z/EVES to analyze and verify the proof obligations.

We present a formal model for component-based development system that provides precise mathematical definitions for concepts like component, connector, software architecture as well as interface, type and behavior. Based on these concepts, we develop a refinement approach that captures the essential nature and principles of component-based design.

As a powerful means of measuring a test set, mutation testing has been applied to program-based testing for a long time. However, with the development of formal specification technique, the formal specifications also play an important role in software testing. For measuring the quality of the specification-based test cases, researchers provide some mutation operators for the logic predicates. With the emergence of the object-oriented formal specifications, these mutation operators cannot completely model the faults arise in an object-oriented specification and from the misunderstanding of the specification. This paper investigates the faults that may occur in the object-oriented specifications, and gives a set of mutation operators for the Object-Z specifications to model these faults. These mutation operators provide an approach to measuring specification-based test cases and validating the Object-Z specifications.

Class testing is the base of object-oriented software testing. It involves three aspects: testing each method, testing the relations among class methods and testing the inheriting relation between class and subclass. Rather than concerning the whole class testing process, most specification-based class testing focuses on the methods of generating test cases from the class specification. As a result, the class testing process and test cases cannot be unified and managed in a consistent and convenient way. This paper introduces a test class framework (TCF) that is used to structure the test cases and test deriving process of the class under testing. This framework clearly denotes the process of deriving test cases and test suites from a class specification. It facilitates the construction and management of test cases. Object-Z notation is used to express the framework and class specification.

This paper introduces an integrated Z support tool, Z User Studio (ZUS), which was developed by the Formal Methods Research Group of Shanghai University. ZUS is an interactive, single-user tool, running under MS-Windows and NT It supports the production of well-formed Z specifications by providing facilities for building, editing, checking and viewing Z specification documents. It displays the Z constructs and symbols, as they would appear in most popular book on Z ZUS has two modes for editing specifications, text-based editor and graphical editor. The graphical editor provides a hierarchical structure directory for every current Z specification. ZUS implements a computer aided test cases generator (TCG).

This paper introduces test classes and a test class framework for generating test cases from Z specifications. We define a test class using object-oriented concept in test framework instead of Phil Stock's test template. Our test framework for Z specifications uniformly defines the test data and oracles in a test class that also contains the information of before states and after states for an operation. Thus, the derivation and construction of test case and test sequence information can be unified in a test framework. We present an example to demonstrate how to generate test cases using the test framework. To support the framework, we have designed and implemented a test case generation system, TCGS, and its functions are briefly described in the paper.

Formal methods use a mathematically based notation to describe the specification of software systems and, based on these they have a notation of an implementation satisfying a specification. Z notation has been widely used in academia and industry. One of the things that we have either to prove formally, or to convince ourselves of in some other way, about every specification written in Z, is that the initial state exists. This paper explores theoretically the test of initial states in Z specifications. The new concepts, constructed function and constrained state space are introduced. The testing approach proposed in this paper can be used to detect the erroneous initial state in Z specifications. By way of examples, the application of testing approach is given.