Alma L. Juarez Dominguez

Research Interests

I am interested in the development of techniques and tools that facilitate reusable independent feature development in automotive systems, providing a means for efficient detection of feature interactions. A feature interaction occurs when features that have been developed and tested in isolation are integrated into a system and cause unexpected or undesired system behaviour. The feature interaction problem becomes more prevalent with the increased complexity in systems, reuse and integration of legacy systems.

I am also interested in the development of theories and formal analysis techniques for distributed systems, particularly ones that communicate through first-in, first-out (FIFO) queues. I want to investigate proof techniques for liveness properties of a protocol forming 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 have studied the use of formal methods and expert domain knowledge to deal with the feature interaction problem in the automotive domain. As part of a NSERC Industrial Postgraduate Scholarship (IPS), I collaborated with General Motors Canada and Critical Systems Labs to develop techniques and tools that provide a means for the detection feature interactions.

Automotive embedded systems consist of software that monitor and control the electrical and mechanical processes. In the automotive domain, a feature is a bundle of system functionality that the driver or the passengers use, and it is marketed by a company. For instance, an automotive feature is Cruise Control (CC). The features that have a degree of control over the motion control systems of the vehicle are generally called Active Safety Features, which request actions to the 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, which form the essence of what is called the feature interaction problem. An example of a feature interaction in automotive active safety features 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.

The main goal of my work is to be able to detect feature interactions during the integration of the automotive features. Steps to achieve the main goal are:

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

   After identifying the characteristics of the automotive active safety features, I have recognized that model checking is an appropriate technique to detect feature interactions between automotive feature designs at design-time. I have selected the model checker Cadence SMV because of its powerful and flexible input language that can describe the semantics of Stateflow and the composition of features. Matlab's Stateflow language is used extensively for designing the controllers of embedded components in the automotive and avionics industry.

   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 automotive active safety features, that is based on the actuators in the mechanical processes controlled by the features, have been published 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: 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 mdl2smv to translate automotive features designed in a subset of the Stateflow language into the notation of Cadence SMV. 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.

   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. Also, because there was not a publicly available set of automotive Stateflow features we could used to validate my results, I created a set of non-proprietary features called the University of Waterloo Feature Model Set (UWFMS). The appendix of my dissertation is included as documentation of the UWFMS package, available at: Download UWFMS.

   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.

3. Detection of all Different Feature Interactions at Design-time: Alfie

   In the automotive domain, a comprehensive view of the problem is required by looking at all different feature interactions before deciding on a resolution strategy. Therefore, I propose a method to detect automatically all different feature interactions by performing analysis of the feature models at design time using model checking. However, generating all different counterexamples proved very challenging, and thus, I divide the problem into two subgoals: (i) Find a summary representing all counterexamples for invariant checking of an extended finite state machine (EFSM), therefore detecting all errors in a model, and (ii) Generalize the method to find a summary of all counterexamples for a pair of Stateflow models of active safety features, therefore detecting a representation of all the feature interactions in the integrated set of features.

More details on the case studies with our own non-proprietary features models, thus validating my approach experimentally, will be given soon.

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.

• Poster presented at ASE 2005: Download(PDF)

List of Publications

Refereed Publications

• A. L. Juarez Dominguez, B. G. Partridge, J. J. Joyce. Creating Safety Assurance Cases for Rebreather Systems. In the Proceedings of the Workshop on Assurance Cases for Software-intensive Systems of the 35th Int'l Conf. on Software Engineering (ICSE). San Francisco, California. May, 2013.
• 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, 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, 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, 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, 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\%)

Non-refereed Publications

• A. L. Juarez Dominguez, N. A. Day. smv-morph: Working with Cadence SMV models in Moscow ML, University of Waterloo. Technical Report CS-2012-24. Waterloo, ON, Canada. December, 2012.
• A. L. Juarez Dominguez, N. A. Day. On-the-fly Counterexample Abstraction for Model Checking Invariants, University of Waterloo. Technical Report CS-2010-11. Waterloo, ON, Canada. April, 2010.
• A. L. Juarez Dominguez, N. A. Day, 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, W. Godard, 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.