Research

ur broad interest is in the use of automated techniques to support analysis of software engineering artefacts including requirements, design and code. Currently most of our work is along one of the following themes:

Scenario-Based Specifications

Scenario notations, such as Message Sequence Charts and UML sequence diagrams are popular as part of requirements specifications. A scenario is a partial story describing how system components, the environment and users work interact in order to provide system level functionality. Their simplicity and intuitive graphical representation facilitates stakeholder involvement and makes them well suited for conveying and documenting requirements. Our interest follows from these desirable characteristics of a specification language and has led us to pursue a number of research questions: How can behaviour models be synthesised from scenarios? What kind of behaviour models can be synthesised when a partial description is available? How can scenario descriptions be combined with other kinds of specifications such as declarative requirements and architecture descriptions? How can an implementation (or a model of it) be checked against a scenario-based specification? What extensions in terms of expressiveness can be defined for scenario-based languages? Some representative publications:[Synthesising Modal Transition Systems from Triggered Scenarios - TSE in press][Specification Patterns can be formal and still easy - SEKE10]

Validation and Verification of Software Call Protocols

Software that has non-trivial requirements with respect to the order in which methods or procedures ought to be used are commonplace. Such is the case for network protocols, API implementations and objects with rich interaction protocols. Verification and validation of individual procedures is hard enough, and is the focus of many verification techniques, notably unit testing. However, specification and analysis of all valid sequences of calls (the call protocol) is extremely complex. In practice, descriptions of the intended behaviour of such systems is incomplete and informal, if documented at all, hindering verification and validation of the code artefacts themselves and the client code that uses the artefacts. We take a model-based engineering approach to this problem developing techniques that can automatically extract abstractions of the call protocol defined in an implementation (or it's specification) and then using these abstractions to support human-in-the-loop validation and model-based testing.

This work was inspired by our collaboration with Microsoft and has been validated using various of their Windows Server protocols. We worked with the Protocol Engineering Team at Microsoft to support their Model Based Testing initiative for quality assurance of protocol documentation. In particular, we collaborated on quality assessment of the behaviour models for Windows Server protocols. We developed a technique for producing finite state machines that abstract automatically a protocol specification or a protocol implementation (in C or .NET) that can be used for validation through inspection or test case generation. We have results showing that experts inspecting these abstractions were capable of identifying specification and/or implementation problems in industrial case studies, including finding problems in MS documentation of public MS Windows Server Protocols. We also have results showing that test case generation from these abstractions support semantic coverage criteria that predict well both structural code coverage and bug finding capability. Hence, there are reasons to believe that they are very effective in test driven development and also for regression testing.

Some representative publications: [Automated Abstractions for Contract Validation, TSE12][Enabledness-based Program Abstractions for Behaviour Validation. TOSEM12]

Controller Synthesis in Software Engineering

Michael Jackson's Machine-World model establishes a framework on which to approach the challenges of requirements engineering. In this model, requirements are prescriptive statements of the world expressed in terms of phenomena on the interface between the machine we are to build and the world in which the real problems to be solved live. Such problems are to be captured with prescriptive statements expressed in terms of phenomena in the world (but not necessarily part of the machine-world interface) called goals $G$ and descriptive statements of what we assume to be true in the world.
Within this setting, a key task in requirements engineering is to understand and document the goals and the characteristics of the domain in which these are to be achieved, in order to formulate a set of requirements for the machine to be built such that assuming that the domain description and goals are valid, the requirements in such domain entail the goals.
Thus, a key problem of requirements engineering can be formulated as a synthesis problem. Given a set of descriptive assumptions on the environment behaviour and a set of system goals, construct an operational model of the machine such that when composed with the environment, the goals are achieved. Such problem is a perfect match to what is known as the controller synthesis problem. Although studied extensively, controller synthesis has not been studied in depth in the context of software engineering. We are interested in understanding how to adapt and extend controller synthesis results to support software engineering tasks related to event-based, arquitecture-level, behaviour models. In particular we are studying applications of controller synthesis to behaviour model elaboration, including the use of partial behaviour models, and also adaptive systems. Some representative publications: [The Modal Transition System Control Problem,FM12][Synthesising Non-Anomalous Event-Based Controllers for Liveness Goals]

Analysis of Resource Consumption for Java like programs

Nowadays, we are surrounded by billons of electronic devices running a diversity of software. These systems may fail but the reason of failure is not always because of a bug or missing functionality. Sometime, a well-conceived piece of software may fail due to a lack of resources to run properly. For instance, the smartphones, although they become more and more powerful, they still have a limited processing power, amount of memory, energy and have to often communicate with other systems, incurring in communication costs that should be controlled. Even in a completely different setting like computer farms (cloud computing) or clusters where resources appear to be unlimited, the core of the business resides on managing them efficiently. Therefore, a quantitative analysis of the computational resources is important either for warrantying the proper execution of applications as well as the right sizing of hardware for a determined task or service.
We aim to develop techniques to analyze resource consumption in real programs. We are interested in scalable inference and verification techniques to obtain resource consumption certificates. We are also interesting resource oriented test case generation. Our main focus is in analyzing dynamic memory consumption, which evolves in a non-monotone fashion in time. This is because automatic memory managers that recycles object when they are non-longer needed (e.g., garbage collector).  

 

Some representative publications:[Quantitative dynamic-memory analysis for Java,CCPE11][Symbolic Polynomial Maximization over Convex Sets and its Application to Memory Requirement Estimation,VLSI09]

Partial Behaviour Modelling

Although software behaviour modelling and analysis has been shown to be successful in uncovering subtle requirements and design errors, adoption by practitioners has been slow. One of the reasons for this is that traditional approaches to behaviour models are required to be complete descriptions of the system behaviour up to some level of abstraction, i.e., the transition system is assumed to completely describe the system behaviour with respect to a fixed alphabet of actions. This completeness assumption is limiting in the context of software development process best practices which include iterative development, adoption of use-case and scenario-based techniques and viewpoint- or stakeholder-based analysis; practices which require modelling and analysis in the presence of partial information about system behaviour.
We believe that there is much to be gained by shifting the focus in software engineering from traditional behaviour models to partial behaviour models, i.e. operational descriptions that are capable of distinguishing known behaviour (both required and proscribed) from unknown behaviour that is yet to be elicited. Our overall aim is to develop the foundations, techniques and tools that will enable the automated construction of partial behaviour models from multiple sources of partial specifications, the provision of early feedback through automated partial behaviour model analysis, and the support incremental, iterative elaboration of behaviour models. Some representative publications:[Weak Alphabet Merging of Partial Behaviour Models,TOSEM12][Distribution of Modal Transition Systems,FM12]

Automated Verification and Diagnosis

Verification is extremely effective in uncovering problems in formal artifacts that are constructed throughout system development (e.g. code, requirements and design specifications) and deployment (e.g. network and infrastructure configurations). However, they provide little or no support for understanding the causes of uncovered problems, let alone fixing them. When verification fails, we are left with examples of how such failure occurs but not with an understanding of why. Tracing back to the artifact under analysis, going from symptom to cause, is a difficult problem. The gap between the syntax and semantics of the languages used for writing artifacts to be verified that is at the heart of the problem. Automated support for diagnosis and repair would reduce significantly human effort involved in software development. A tool that proposes plausible explanations and alternative, sound, fixes to problems identified in verification activities would allow engineers to focus on key decisions rather than on tedious error tracing and error prone corrections. The problem of explaining examples (be them failures or of any other kind) in terms of a given theory (e.g. a program, specification, or rule-set) and adapting the theory to avoid the symptoms is core to symbolic learning, a field of Artificial Intelligence which has undergone a revolution in the last decade. Yet, the use of these learning methods has not permeated software systems development even though the correspondence between the learning task and verify-diagnose-repair tasks is straightforward: The theory is the artifact constructed, deployed or executed, while the symptom is the result of verification. We are currently investigating the comnination of verification and symbolic learning techniques (more specifically model checking and inductive logic programming) to evolve, elaborate and fix requirements specifications. Some representative publications:[Generating obstacle conditions for requirements completeness,ICSE12][Deriving Non-Zeno Behavior Models from Goal Models using ILP,FACS10]

English