Modeling & Analysis in
1. Model-Driven Development
The main goal behind MDD is to make models, rather than code, the primary artifact around which most software development activities are centered. Through the emphasis on models, MDD attempts to manage the complexity of software and its development by supporting abstraction and automation. To this end, it combines techniques not only from software modeling (e.g., UML and Domain-Specific Modeling), but also from a range of areas such as generative programming, software product lines, programming languages, and formal methods.
The long-term goal of our work is to help maximize the potential of MDD. To do this, we are currently engaged in the following projects:
2. Compositional development and analylsis
using behavioural interface specifications
3. Applying Discrete Event System Theory for Software Engineering
The goal of this research theme is to leverage the existing work on the supervisory control problem to simplify software development. Discrete Event System control theory (DES) defines the supervisory control problem (SCP) as follows: given an uncontrolled system G and a specification L, find a supervisor S such that S restricts G in such a way that all its executions satisfy L and that S is minimally restrictive. Control theory offers a large body of research on the SCP with surprisingly little application to software development.
We have been investigating the use of automatically generated supervisors for the automatic enforcement of software specifications that restrict the order in which certain kinds of events are allowed to occur. Depending on how these events are defined, different kinds of specifications can be enforced.
For instance, in recent work we considered events based on the access to resources shared by concurrently executing processes. Concurrent source code devoid of any concurrency control is manually instrumented with events. From this, the uncontrolled system G is obtained. The supervisor S generated via DES control theory will contain a minimally restrictive control scheme that causes G to satisfy the specification L and ensures deadlock freedom (if deadlock is unavoidable, S will prevent all of G's executions). The control scheme is then realized in the original source code by injecting appropriate synchronization constructs into the concurrent source code before event occurrences. To the best of our knowledge, this approach represents the first use of DES theory for the generation of concurrency control code. Apart from the initial event instrumentation, the process is completely automatic, programming language independent, and inherits the strong theoretical properties of the standard supervisory control framework developed.
This research is joint work with Dr. Karen
Rudie (Queen's ECE) and funded by
the Natural Sciences and Engineering Research
Council of Canada (NSERC).