I am interested in all aspects of software modelling, documentation, and analysis.  I am particularly interested in what I call practical formalisms -- specification and design notations that are practitioner-friendly and yet have a precise semantics that is suitable for automated analysis. Most recently, I am interested in these problems as they apply to automotive software and features.

Requirements Analysis Much of my research work has focused on computer-aided tools and techniques for analyzing software requirements and specifications. I work with model checkers and reachability analyzers that exhaustively check that a specification adheres to desired system properties (e.g., safety, liveness, and timing properties, expressed as logic formulae). These tools hold the promise of providing to software practitioners push-button mathematical verification of their specifications and designs. However, such verification is computationally expensive in both space and time, and much of my work involves understanding how to structure and abstract specifications to make their model checking feasible.

Feature Interactions The feature interaction problem is prevalent in software systems in which features (or devices) are developed as independent extensions or add-ons to an application, when in fact the features subtly interfere with each other over shared data. I am interested in automated techniques for detecting interactions among features -- especially techniques that efficiently checks all valid feature combinations. (Product-line symbolic model checking)

Resolution Analysis As part of our work on coordinating features, we are experimenting with generic strategies for resolving feature interactions at runtime. These results could possibly be used to coordinate features and devices connected via an IoT.

Semantically Configurable Languages and Tools I am interested in generating analysis tools from the definition of a notation's semantics, in the manner that we currently generate parsers from grammar definitions. As a first step, we have unified the execution semantics of several model-based notations as a parameterized model of next-state relations, and we have identified a collection of composition primitives that are common to many notations. We are working on automating the generic model of execution semantics and the composition primitives we have identified so far, so that users can generate a custom analysis tool by selecting semantics parameters and appropriate composition primitives.
2002 J.M. Atlee

Updated: 4.21.02...