Publications

 Nowadays electrical communications systems are being used more and more widely to provide global connections between very large numbers of people. In order for such systems to operate efficiently and effectively, control must be distributed to local sub-networks, with each sub-network being responsible only for a small part of the system and passing on the responsibility to some adjacent part of the system whenever it is unable to perform the whole of a requested task itself. In this paper we describe a generic hierarchic communications system which is structured in this way and we give a formal specification in RSL of its structure and of the message-passing mechanism by which responsibility is delegated.

Efforts to promote sustainable broadband Internet adoption urge new attention to the classic diffusion of innovations paradigm. For this study, innovation attributes were reconceptualized following Social Cognitive Theory (SCT). In a sample of inner-city residents, the model accounted for 36% of the variance in intentions to adopt broadband technology and services, primarily from the SCT variables of expected outcomes and self-efficacy. Prior habitual use of the Internet was also a predictor. Price sensitivity was unrelated to adoption. Among demographic variables, only age had a significant (negative) relationship to broadband adoption after accounting for the SCT variables. Recommendations for the design and monitoring of sustainable broadband adoption interventions are made based on these findings.

Component-based development allows one to build software from existing components and promises to improve software reuse and reduce costs. For critical applications, the user of a component must ensure that it fits the requirements of the application. To achieve this, testing is a well-suited means when the source code of the components is not available. Robustness testing is a testing methodology to detect the vulnerabilities of a component under unexpected inputs or in a stressful environment. As components may fail differently in different states, we use a state machine based approach to robustness testing. First, a set of paths is generated to cover transitions of the state machine, and it is used by the test cases to bring the component into a specific control state. Second, method calls with invalid inputs are fed to the component in different states to test the robustness. By traversing the paths, the test cases cover more states and transitions compared to stateless API testing. We apply our approach to several components, including open source software, and compare our results with existing approaches.

Component based development allows to build software upon existing components and promises to improve software reuse and reduce costs. To gain reliability of a component based system, verification technologies such as testing can be applied to check underlying components and their composition. Conformance testing checks the consistency between the behavior and component specifications. On the other hand, robustness testing detects vulnerability of software with unexpected input or stressful environment. Existing robustness testing tools aim to crash components with preset values of different data types. But they do not take into account component states, which are vital to the detecting robustness problem of a component. We propose a state machine based approach to detect robustness problems of components. Firstly, a set of paths is generated to cover transitions of the state machine. Test inputs which follow the paths achieve high coverage of the system states and examine more transitions than stateless API testing. Secondly, invalid inputs and inopportune method calls are fed to the component in different states to test the robustness. When unexpected exceptions arise in the test runs, robustness failures are reported. We do a case study on a component from an open source software and it results in positive results.

We present AutoPA, a tool to analyze and validate the consistency and functional correctness of use case designs. The tool directly generates an executable prototype from the requirements. The requirements are captured from different views of the application. Each view is constructed as UML diagram annotated with OCL specifications. Based on a formal semantics, the tool is implemented so that both syntactic and semantic consistency among the provided views can be guaranteed. Afterwards the requirements are analyzed and translated into an executable prototype, allowing the user to interactively validate the functional properties of the requirements model. We illustrate the benefits of the tool using a real-world sized example.

Integrating formal methods into UML opens up a way to complement UML-based software development with precise semantics, development methodologies, as well as rigorous verification and refinement techniques. In this paper, we present an approach to integrate a formal method to practical component-based model driven development through defining a UML profile that maps the concepts of the formal method as UML stereotypes, and implementing the profile into a CASE tool. Unlike most of the previous works in this vein, which concentrate on verifying the correctness of the models built in the development process, we focus on how the full development process can be driven by applying the refinement rules of the formal method in an incremental and interactive manner. The formal method we adopt in this work is the refinement for Component and Object Systems (rCOS). We demonstrate the development activities in the CASE tool using an example.

This paper presents a formal semantics of UML sequence diagram. In abstract syntax form, a well-formed sequence diagram corresponds to an ordered hierarchical tree structure. The static semantics of a sequence diagram is to check whether it is consistent with the class diagram declaration as well as with its well-formed tree structure. Meanwhile, the dynamic semantics is defined in terms of the state transitions that are carried out by the method invocations in the diagram. When a message is executed, it must be consistent with system state, i.e., object diagram and the state diagrams of its related objects. The semantics clearly captures the consistency between sequence diagram with class diagram and state diagram. Therefore, it is useful to develop the model consistent checking functions in UML CASE tools. And it also can be used to reason about the correctness of a design model with respect to a requirement model.

Consider an object-oriented model with a class diagram, and a set of object sequence diagrams, each representing the design of object interactions for a use case. This article discusses how such an OO design model can be automatically transformed into a component-based model for the purpose of reusability, maintenance, and more importantly, distributed and independent deployment. We present the design and implementation of a tool that transforms an object-oriented model to a component-based model, which are both formally defined in the rCOS method of model driven design of component-based software, in an interactive, stepwise manner. The transformation is designed using QVT Relations and implemented as part of the rCOS CASE tool.

Consider a requirements model with a set of interfaces representing use cases, and a set of system sequence diagrams specifying the scenarios of the interfaces, this paper discusses how to automatically transform such a model into an inial design model by generating a protocol state machine for each interface from its sequence diagrams, and deriving a controller class as an implementation of the interface. The generated model can be severed as the starting point for the detailed object-oriented design. The contracts of the controller class ensure that the behaviour defined by the sequence diagrams is fully complied with through pre/post-conditions. The transformation takes into account the concurrency and critical area of the respective diagrams. We present the design and implementation of the transformation, which is specified using the graphical notation of QVT Relations and integrated into a CASE tool.

 Component-based development allows to build software from existing components and promises to improve software reuse and reduce costs. For critical applications, the user of a component must ensure that it fits the requirements of the application. To achieve this, testing is a well- suited means when the source code of the components is not available. Robustness testing is a testing methodology to detect vulnerabilities of a component under unexpected inputs or in a stressful environment. As components may fail differently in different states, we use a state machine based approach to robustness testing. Firstly, a set of paths is generated to cover transitions of the state machine, and it is used by the test cases to bring the component into a specific control state. Secondly, method calls with invalid inputs are fed to the component in different states to test the robustness. By traversing the paths, the test cases cover more states and transitions compared to stateless API testing. We apply our approach to several components, including open source software, and compare our results with existing approaches.

 Fault-tolerance and timing have often been considered to be implementation issues of a program, quite distinct from the functional safety and liveness properties. Recent work has shown how these non-functional and functional properties can be verified in a similar way. However, the more practical question of determining whether a real-time program will meet its deadlines, i.e., showing that there is a feasible schedule, is usually done using scheduling theory, quite separately from the verification of other properties of the program. This makes it hard to use the results of scheduling analysis in the design, or redesign, of fault-tolerant and real-time programs. In this paper we show how fault-tolerance, timing, and schedulability can be specified and verified using a single notation and model. This allows a unified view to be taken of the functional and nonfunctional properties of programs and a simple transformational method to be used to combine these properties. It also permits results from scheduling theory to be interpreted and used within a formal proof framework. The notation and model are illustrated using a simple example.