At a glance:

Quicklinks

Changelog

  • Alma's profile in the Women in Computer Science (WICS) website at the University of Waterloo

"Life is not measured by the number of breaths we take but by the moments that take our breath away"

-- Anonymous

Research Interests

I am interested in the development of techniques and tools that will facilitate reusable independent feature development in automotive embedded systems, by providing a means for efficient detection of feature interactions. A feature interaction occurs when the feature in an environment of other features does not perform as it does when the feature operates in isolation. The feature interaction problem becomes more prevalent with the increased complexity in systems. Given that features often evolve as a product line, feature interaction is an ongoing problem.

I am also interested in the development of theories and formal analysis techniques for distributed systems, particularly ones that communicate asynchronously through first-in, first-out (FIFO) queues. Many IP-based protocols, defining the interaction between concurrent processes, often create graphs of connections where a component communicates only with its immediate neighbours. I want to investigate proof techniques for liveness properties of a protocol for chains of connections of an unknown number of finite state processes that communicate asynchronously via FIFO queues.

For the interested reader, refer to my List of Publications

Current Work

For my doctorate research, I am studying the use of formal methods and expert domain knowledge to deal with the feature interaction problem in the automotive domain. Currently, as part of my NSERC Industrial Postgraduate Scholarship (IPS), I am collaborating with General Motors Canada and Critical Systems Labs to develop techniques and tools that will provide a means for the detection feature interactions.

Feature Interaction Problem in the Automotive Domain

Automotive embedded systems consist of software, as well as electrical and mechanical processes monitored by the software. In the automotive domain, a feature is a bundle of system functionality recognized by the driver and marketed by a company; it is normally implemented in software, and provides advanced functionality to the vehicle. For instance, an automotive feature is Cruise Control (CC). These features have a degree of control over the mechanical components that operate the dynamics of the vehicle, and the features are generally called Advanced Safety Features. Examples of the mechanical components are brakes, throttle and steering.

When features that have been developed and tested in isolation are integrated into a system, the features’ combination can cause undesired or unexpected system behaviour. These unexpected and undesired interactions form the essence of what is called the feature interaction problem. An example of a feature interaction in an automotive embedded system is having simultaneous requests to apply the brakes and the throttle. A feature interaction can cause problems ranging from driver discontent to a fatal accident.

Traditionally, in automotive systems, reliability and correctness checks are performed using extensive testing and techniques such as probabilistic reliability modelling and Failure Modes and Effects Analysis (FMEA). These techniques focus on individual feature failures and do not help identify feature interactions during integration. Given that features often evolve as a product line, feature interaction is an ongoing problem.

Detection of Feature Interaction in the Automotive Domain

The main goal of my work is to be able to verify the absence of feature interactions in the integration of the automotive features and the lack of errors in their design. After identifying the unique characteristics of the automotive domain, we have recognized that model checking is an appropriate technique to detect feature interactions between automotive feature designs. We have selected the model checker SMV because of its powerful features for model checking and flexible input language, in which we can describe the semantics of Stateflow and of the composition of features. Matlab's Stateflow language is used extensively for designing the controllers of embedded components in the automotive and avionics industry. Steps to achieve the main goal are:

  1. Modelling of Automotive Features and Definition of Feature Interaction in the Automotive Domain

    The description of two interesting modelling aspects that arise when creating a description in SMV of the behaviour of automotive features designed in Stateflow, as well as our proposed general, systematic definition of feature interactions for the automotive domain that is based on the actuators in the mechanical processes controlled by the features have been publised in the Proceedings of the Workshop on Modeling in Software Engineering (MISE 2008) at 20th IEEE/ACM International Conference on Automated Software Engineering conference proceedings.

    • MiSE 2008 (accepted): Download(PDF)

      Modelling Feature Interactions in the Automotive Domain

      © 2008 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

      Abstract: We propose to use model checking to detect feature interactions in a set of features under design for an automotive embedded system. In this paper, we present (1) the characteristics of the feature interaction problem in the automotive domain that make model checking an appropriate detection technique; (2) our proposal for a general, systematic definition of feature interactions for this domain based on the set of actuators in the vehicle influenced by the features; and (3) our solutions to two modelling issues that arise when creating a description in SMV of the behaviour of an integrated set of automotive features designed in MATLAB's Stateflow.

  2. Translation of Automotive Features from Matlab's Stateflow to SMV: mdl2smv

    We have created a tool to translate automotive features designed in Stateflow into SMV that we call mdl2smv. The translated SMV models will allow us to verify properties of the automotive features at the same level of description as the design, so that the findings of our analysis can be applied to the design of the final automotive components. A couple of papers on this topic are summarized next. NOTE: For a description of our translator implementation, as well as more information about the supported Stateflow elements, its limitations and the semantics issues, please look at the mdl2smv implementation page.

    The description of how the elements of Stateflow are mapped to elements in the SMV notation to translate feature design models in Matlab’s Stateflow have been publised in the Proceedings of the 26th International System Safety Conference (ISSC 2008).

    • ISSC 2008: Download(PDF)

      Translating Models of Automotive Features in MATLAB’s Stateflow to SMV to Detect Feature Interactions

      Abstract: Feature interactions are becoming more prevalent as systems increase in complexity, and can be a source of significant risk. When features that are designed to run independently are integrated within a system, the combination of their behaviours may interfere with each other. We propose to use the formal verification technique of symbolic model checking to examine exhaustively all behaviours of an integrated set of features to detect feature interactions. In this paper, we describe how to translate automotive features described in MATLAB's Stateflow language into the input language of the model checker SMV. MATLAB's Stateflow is used extensively for designing embedded components in various domains such as the automotive and avionics industries. SMV has powerful features for model checking and has a flexible input language, in which we can describe the semantics of Stateflow and of the composition of features. The translated SMV models contain the same level of description as the design, so that the findings of our analysis can be directly understood in terms of the feature design in Stateflow.

We are currently working on case studies with our own non-proprietary features models to validate our approach experimentally.

Previous Work

I was working on the project "Managing Feature Interactions among Distributed Services", which focuses on modular feature development in Distributed Feature Composition (DFC), a new architecture that AT&T is investigating for telecommunications applications. As part of this work, we wrote a Technical Report CS-2004-40, where we describe our effort to represent and model check the DFC architecture in SPIN. We summarized the results accomplished so far, as well as proposed what are the steps to follow.

  • Tech Report CS-2004-40: Download(PS) | Download(PDF)

    Model Checking the Distributed Feature Composition (DFC) Architecture in SPIN

    Abstract: In this report, we describe our effort to represent and model check the Distributed Feature Composition (DFC) architecture in SPIN. DFC is an architecture for describing telecommunications services. SPIN is a model checker for models described in the language PROMELA.

My Master's research concentrated on identifying correctness criteria in the telecommunications system domain, focusing on the Distributed Feature Composition (DFC) architecture, developed by Jackson and Zave at AT&T. The main goal of my work was to create a definition of DFC compliance for features with respect to the call protocol using a set of linear temporal logic (LTL) properties. First, I described and model checked configurations of a fixed number of DFC feature models in the model checker SPIN. Second, in order to conclude more general properties about n features, I decomposed the problem into two main parts: verify properties of individual components using SPIN, and then use the HOL theorem prover to carry out compositional reasoning and conclude the set of LTL properties proposed about the DFC architecture. The tittle of my Master's thesis is "Verification of DFC Call Protocol Correctness Criteria".

  • Master's Thesis: Download(PS) | Download(PDF)

    Verification of DFC Call Protocol Correctness Criteria

    Abstract: Distributed Feature Composition (DFC) is an architecture developed by Jackson and Zave at AT&T to describe and implement telecommunication services. DFC supports modular development, where features that are independently implemented can be composed. The main goal of our work is to create a definition of DFC compliance for features with respect to the signalling call protocol using a set of linear temporal logic (LTL) properties and to verify that our proposed protocol properties hold for segments of DFC with n features communicating through unbounded queues. Our main contribution is a compositional reasoning method that decomposes the problem into two parts: (1) Model check features individually in an abstract environment to verify that they are DFC compliant with respect to the call protocol, and (2) Use the properties of the individual features in an inductive proof to conclude that the call protocol properties hold over segments of the DFC architecture.

I also have studied compositional reasoning techniques for distributed systems more generally, investigating both the theory and practice of analyzing real systems. Some of these ideas have been publised on the 20th IEEE/ACM International Conference on Automated Software Engineering conference proceedings, but I plan to work more on it in the future.

  • ASE 2005 Short Paper (accepted): Download(PS) | Download(PDF)

    Compositional Reasoning for Port-based Distributed Systems

    © ACM, 2005. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution.

    Abstract: Many distributed systems using IP-based communication protocols consist of chains of components that run concurrently and communicate asynchronously with their neighbours through ports. We present a compositional reasoning method using model checking and theorem proving to verify liveness properties of a communication protocol for chains of connections consisting of an unknown number of components. We outline how our method is used to verify properties of the call protocol of AT&T's Distributed Feature Composition (DFC) architecture.

List of Publications

Refereed Publications

  • A. L. Juarez Dominguez. Feature Interaction Detection in the Automotive Domain. In the Proceedings of the Doctoral Symposium of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE). L'Aquila, Italy. September, 2008.
  • A. L. Juarez Dominguez, N. A. Day, J. J. Joyce. Modelling Feature Interactions in the Automotive Domain. In the Proceeedings of the 2008 International Workshop on Modeling in Software Engineering (MiSE). Leipzig, Germany. May 2008.
  • A. L. Juarez Dominguez, N. A. Day. Compositional Reasoning for Port-based Distributed Systems. In the Proceeedings of the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE) 2005. (short paper), Long Beach, California. June, 2005. (acceptance rate: 22\%)
  • A. L. Juarez Dominguez, Verification of the DFC Port Protocol Correctness Criteria, Master's Thesis, University of Waterloo, Waterloo, ON, Canada. April, 2005.

Non-refereed Publications

  • A. L. Juarez Dominguez, N. A. Day, and R. T. Fanson. Translating Models of Automotive Features In MATLAB's Stateflow to SMV to Detect Feature Interactions. In Proceedings of the 26th International System Safety Conference (ISSC 2008), Vancouver, BC, Canada. August, 2008.
  • A. L. Juarez Dominguez, N. A. Day, and R. Fanson. A Preliminary Report on Tool Support and Methodology for Feature Interaction Detection, University of Waterloo. Technical Report CS-2007-44. Waterloo, ON, Canada. December, 2007.
  • A. L. Juarez Dominguez, J. J. Joyce, and R. Debouk. Feature Interaction as a Source of Risk in Complex Software-intensive Systems. In Proceedings of the 25th International System Safety Conference (ISSC 2007), Baltimore, USA. August, 2007.
  • A. L. Juarez Dominguez, W. Godard, and N. A. Day. Model Checking the Distributed Feature Composition Architecture (DFC) in Spin, University of Waterloo. Technical Report CS-2004-40. Waterloo, ON, Canada. April, 2004.
Home | Research | Presentations | Service | Links |