Ethan Jackson at Microsoft Research
Ethan Jackson
ejackson@microsoft.com One Microsoft Way Redmond, WA 98052-6399 U.S. +1 (425) 703-5978
research :: My research focuses on formal model-based development of software systems. I am interested in the use of models and formal methods to engineer correct systems and to evaluate the impact of design choices prior to implementation. To this end, we develop the FORMULA tool suite, which provides an expressive modeling language equipped with automated formal analysis. Through FORMULA, we prototype novel language-level approaches for formal modeling, and we expose state-of-the-art formal methods for automated reasoning about models of software systems.
projects ::


FORMULA
- A specification language / tool suite for building domain-specific languages and models, and analyzing their properties. Go to the FORMULA website.


P Programming Language
- A high-level DSL for building asynchronous concurrent state machines. Can be used to build Windows device drivers, in which case C code is emitted. Also emits Zing code to model check properties of programs.


Executable biology
- Working with Jasmin Fisher and Ben Hall from the Programming Principles and Tools Group (MSR Cambridge) on building and analyzing executable models of biological systems.

explore! ::


MODELS 2013
- Submit a paper to MODELS 2013; abstract deadline is March 4th and submission deadling is March 14th. Also, consider submitting to the ACM Student Research Competition by July 15th. The SRC is chaired by Davide Di Ruscio and myself.


Journal of Software and Systems Modeling
- Consider submitting your journal articles to the Journal of Software and Systems Modeling. Editors-in-chief: Robert France and Bernhard Rumpe.


FANG Design Challenges
- Visit DARPA's "Fast, Adaptable, Next-Generation Ground Vehicle" (FANG) design challenges and build a next-generation amphibious vehicle.

publications :: Please browse the list of publications below. Click a link for more details.
28. Ankush Desai, Vivek Gupta, Ethan K. Jackson, Shaz Qadeer, Sriram Rajamani, and Damien Zufferey: P: Safe Asynchronous Event-Driven Programming, PLDI 2013.
In press; available later.
abstract ::

Available later.

27. Ethan K. Jackson, Tihamer Levendovszky, and Daniel Balasubramanian: Automatically Reasoning about Metamodeling, Journal of Software and Systems Modeling, 2013.
In press; available later.
abstract ::

Metamodeling is foundational to many modeling frameworks, and so it is important to formalize and reason about it. Ideally, correctness proofs and test-case generation on the metamodeling framework should be automatic. However, it has yet to be shown that extensive automated reasoning on metamodeling frameworks can be achieved. In this paper we present one approach to this problem: Metamodeling frameworks are specified modularly using algebraic data types and constraint logic programming (CLP). Proofs and test-case generation are encoded as \textit{open world} query operations and automatically solved.

26. Gabor Simko, David Lindecker, Tihamer Levendovszky, Ethan K. Jackson, Sandeep Neema and Janos Sztipanovits: A Framework for Unambiguous and Extensible Specification of DSMLs for Cyber-Physical Systems, ECBS 2013.
Available later
abstract ::

Available later.

25. Gabor Simko, Tihamer Levendovsky, Sandeep Neema, Ethan K. Jackson, Ted Bapty, Joseph Porter and Janos Sztipanovits: Foundation For Model Integration: Semantic Backplane, 32nd Computers and Information Conference (ASME IDETC/CIE 2012).
Download
abstract ::

One of the primary goals of the Adaptive Vehicle Make (AVM) program of DARPA is the construction of a model-based design flow and tool chain, META, that will provide significant productivity increase in the development of complex cyber-physical systems. In model-based design, modeling languages and their underlying semantics play fundamental role in achieving compositionality. A significant challenge in the META design flow is the heterogeneity of the design space. This challenge is compounded by the need for rapidly evolving the design flow and the suite of modeling languages supporting it. Heterogeneity of models and modeling languages is addressed by the development of a model integration language � CyPhy � supporting constructs needed for modeling the interactions among different modeling domains. CyPhy targets simplicity: only those abstractions are imported from the individual modeling domains to CyPhy that are required for expressing relationships across sub-domains. This �semantic interface� between CyPhy and the modeling domains is formally defined, evolved as needed and verified for essential properties (such as well-formedness and invariance). Due to the need for rapid evolvability, defining semantics for CyPhy is not a �one-shot� activity; updates, revisions and extensions are ongoing and their correctness has significant implications on the overall consistency of the META tool chain. The focus of this paper is the methods and tools used for this purpose: the META Semantic Backplane. The Semantic Backplane is based on a mathematical framework provided by term algebra and logics, incorporates a tool suite for specifying, validating and using formal structural and behavioral semantics of modeling languages, and includes a library of metamodels and specifications of model transformations.

24. Janos Mathe, Janos Sztipanovits, Mia Levy, Ethan K. Jackson and Wolfram Schulte: Cancer Treatment Planning: Formal Methods to the Rescue, SEHC 2012 (an ICSE 2012 Workshop).
Download
abstract ::

This paper describes the ongoing development of ATTENTION, a new kind of clinical decision support system for synthesizing and managing longitudinal treatment plans, such as cancer treatment plans. ATTENTION combines state-of-the-art formal modeling and constraint solving with clinical information systems to synthesize complex cancer treatment plans that are also executable.

23. Ethan K. Jackson, Wolfram Schulte and Nikolaj Bjorner: Detecting Specification Errors in Declarative Languages with Constraints, MODELS 2012.
Download
abstract ::

Declarative specification languages with constraints are used in model-driven engineering to specify formal semantics, define model transformations, and describe domain constraints. While these languages support concise specifications, they are nevertheless prone to difficult semantic errors. In this paper we present a type-theoretic approach to the static detection of specification errors. Our approach infers approximations of satisfying assignments and represents them via a canonical regular type system. Type inference is experimentally efficient and type judgments are comprehensible by the user.

22. Ethan K. Jackson and Wolfram Schulte: Understanding Specification Languages Through Their Model Theory, Monterey Workshop 2012.
Download
abstract ::

This paper studies the design of specification languages through their model theory. We show how language constructs and specification idioms are deeply rooted in the underlying model theory. We also show that some problems are fundamentally difficult to specify due to the underlying foundation of the language. The languages we study are Alloy, Maude, and FORMULA. FORMULA attempts to handle a large class of specifications problems while utilizing constraint solvers for formal analysis.

21. Ethan K. Jackson, Tihamer Levendovszky, and Daniel Balasubramanian: Reasoning about Metamodeling with Formal Specifications and Automatic Proofs, MODELS 2011.
Download
abstract ::

Metamodeling is foundational to many modeling frameworks, and so it is important to formalize and reason about it. Ideally, correctness proofs and test-case generation on the metamodeling framework should be automatic. However, it has yet to be shown that extensive automated reasoning on metamodeling frameworks can be achieved. In this paper we present one approach to this problem: Metamodeling frameworks are specified modularly using algebraic data types and constraint logic programming (CLP). Proofs and test-case generation are encoded as CLP satisfiability problems and automatically solved.

20. Ethan K. Jackson, Nikolaj Bjorner, and Wolfram Schulte: Canonical Regular Types, ICLP 2011.
Download
abstract ::

Regular types represent sets of structured data, and have been used in logic programming (LP) for verification. However, first-class regular type systems are uncommon in LP languages. In this paper we present a new approach to regular types, based on type canonization, aimed at providing a practical first-class regular type system.

19. Ethan K. Jackson, Eunsuk Kang, Markus Dahlweid, Dirk Seifert, and Thomas Santen: Components, Platforms and Possibilities: Towards Generic Automation for MDA, EMSOFT 2010.
Download
abstract ::

Model-driven architecture (MDA) is a model-based approach for engineering complex software systems. MDA is particularly attractive for designing embedded systems because models can be easily evolved as hardware and software requirements evolve. However, efforts to apply MDA in industrial settings expose several open problems surrounding tooling: Engineers need automated techniques that are scalable, general, and extensible. In this paper we describe the FORMULA framework as a novel approach towards general automation for MDA. We develop a running example and benchmarks to compare our tools with other state-of-the-art approaches.

18. Eunsuk Kang, Ethan K. Jackson, and Wolfram Schulte: Generalizing Design Space Exploration, 14th Monterey Workshop, 2010.
Post-proceedings under review
abstract ::

Design-space exploration (DSE) is the exploration of design alternatives prior to implementation. The power to operate on the space of possible designs decisions makes DSE useful for many software engineering tasks, including rapid prototyping, optimization, and system integration. In this paper we introduce a novel framework for generalizing DSE techniques: Design spaces are specified as domain specific languages (DSLs) with expressive constraints. Next, a symbolic execution engine generates quantifier free formulas whose solutions are non-trivial designs. These formulas are evaluated by a state-of-the-art satisfiability modulo theories (SMT) solver. A novel exploration algorithm guides the solver towards distinctly different designs.

17. Ethan K. Jackson, Wolfram Schulte, Daniel Balasubramanian, and Gabor Karsai: Reusing Model Transformations While Preserving Properties, FASE 2010.
Download
abstract ::

Model transformations are indispensable to model-based development (MBD) where they act as translators between domain-specific languages (DSLs). As a result, transformations must be verified to ensure they behave as desired. Simultaneously, transformations may be reused as requirements evolve. In this paper we present novel algorithms to determine if a reused transformation preserves the same properties as the original, without expensive re-verification. We define a type of behavioral equivalence, called lifting equivalence, relating an original transformation to its reused version. A reused transformation that is equivalent to the original will preserve all compatible universally quantified properties. We describe efficient algorithms for verifying lifting equivalence, which we have implemented in our FORMULA [1, 2] framework.

16. Ethan K. Jackson, and Daniel Balasubramanian: Lost In Translation: Forgetful Semantic Anchoring, ASE 2009.
Download
abstract ::

Assigning behavioral semantics to domain-specific languages (DSLs) opens the door for the application of formal methods, yet is largely an unresolved problem. Previously proposed solutions include semantic anchoring, in which a transformation from the DSL to an external framework that can supply both behavioral semantics and apply formal methods is constructed. The drawback of this approach is that it loses the structural constraints of the original DSL along with the details of the transformation, which can lead to erroneous results when formal methods are applied. We demonstrate this problem of "forgetful� semantic anchoring using existing approaches through a translation from dataflow systems to interface automata. We then describe our modeling tool FORMULA and apply it to the same example, showing how forgetful semantic anchoring can be avoided.

15. Ethan K. Jackson, Markus Dahlweid, Dirk Seifert, Thomas Santen, Nikolaj Bjorner, and Wolfram Schulte: Specifying and Composing Non-functional Requirements in Model-Based Development, Software Composition 2009.
Download
abstract ::

Non-functional requirements encompass important design concerns such as schedulability, security, and communication constraints. In model-based development they non-locally impact admissible platform mappings and design spaces. In this paper we present a novel and formal approach for specifying non-functional requirements as constraint systems over the space of models. Our approach, based on structured logic programming, allows interacting requirements to be specified independently from each other and composed together. Correct-by-construction operators eliminate some composition mistakes. Our approach is implemented in our formal modeling tool FORMULA, which can analyze the impacts of interacting non-functional requirements on platform mappings and design spaces.

14. Ethan K. Jackson, Wolfram Schulte, and Janos Sztipanovits: The Power of Rich Syntax for Model-based Development, MSR Technical Report, 2009.
Download
abstract ::

During the last century, many general purpose programming languages have been developed, all having rigid syntax and often a von-Neuman view of the world. With the rise of model-based development this changes: Feature oriented programming, domain specific languages, and platform-based design use rich and custom syntaxes to capture domain specific abstractions, refinement mappings, and design spaces. In this paper we show how a formalization of rich syntax can be used to compose abstractions, validate refinement maps, and construct design spaces. We describe a tool FORMULA for computing these properties, and present a series of examples from automotive embedded systems.

13. Ethan K. Jackson, and Janos Sztipanovits: Formalizing the Structural Semantics of Domain-specific Modeling Languages, Journal of Software and Systems Modeling, 2009.
Download
abstract ::

Model-based approaches to system design are now widespread and successful. These approaches make extensive use of model structure to describe systems using domain-specific abstractions, to specify and implement model transformations, and to analyze structural properties of models. In spite of its general importance the structural semantics of modeling languages are not well-understood. In this paper we develop the formal foundations for the structural semantics of domain specific modeling languages (DSML), including the mechanisms by which metamodels specify the structural semantics of DSMLs. Additionally, we show how our formalization can complement existing tools, and how it yields algorithms for the analysis of DSMLs and model transformations.

12. Daniel Lucredio, Ethan K. Jackson, and Wolfram Schulte: Playing with Fire: Harnessing the Hottest Technologies for Ultra-Large-Scale Systems , Monterey Workshop 2008.
Download
abstract ::

Creating ultra-large-scale systems requires technological advances across the board [13]. The challenge is so grand that emerging technologies address small subproblems, such as: providing a service orchestration layer, guaranteeing quality of service (QoS), and facilitating decentralized discovery. Engineers wishing to implement a complete system must (1) understand the subproblems, (2) become experts with the latest technologies, (3) and integrate the technologies into a whole. In this paper we describe a model-based approach that reduces these engineering burdens through abstractions and code generation. Our framework took approximately 3-man months to implement, but integrates almost a dozen state-of-the-art technologies. Users of the framework do not have to solve the integration problem, and the framework with is driven by models that are technology independent.

11. Ethan K. Jackson, and Wolfram Schulte: Compositional Modeling for Data-Centric Business Applications , Software Composition 2008.
Download
abstract ::

Data-centric business applications comprise an important class of distributed systems that includes on-line stores, document management systems, and patient portals. However, their complexity makes it difficult to design and implement them. We address these issues from a model-driven perspective by developing a formal, compositional, and domain-specific set of abstractions for the specification and analysis of data-centric business applications. Our technique allows us to formally analyze the specified system at design time; in particular we can analyze whether the system is resilient to abnormal conditions, i.e. that key system invariants can always be re-established

10. Ethan K. Jackson, and Wolfram Schulte: Model Generation for Horn Logic with Stratified Negation , FORTE 2008.
Download
abstract ::

Model generation is an important formal technique for finding interesting instances of computationally hard problems. In this paper we study model generation over Horn logic under the closed world assumption extended with stratified negation. We provide a novel three- stage algorithm that solves this problem: First, we reduce the relevant Horn clauses to a set of non-monotonic predicates. Second, we apply a fixed-point procedure to these predicates that reveals candidate solutions to the model generation problem. Third, we encode these candidates into a satisfiability problem that is evaluated with a state-of-the-art SMT solver. Our algorithm is implemented, and has been successfully applied to key problems arising in model-based design.

9. Ethan K. Jackson, and Janos Sztipanovits: Constructive Techniques for Meta- and Model-level Reasoning , MODELS 2007.
Download
abstract ::

The structural semantics of UML-based metamodeling were recently explored [1], providing a characterization of the models adhering to a metamodel. In particular, metamodels can be converted to a set of constraints expressed in a decidable subset of first-order logic, an extended Horn logic. We augment the constructive techniques found in logic programming, which are also based on an extended Horn logic, to produce constructive techniques for reasoning about models and meta-models. These methods have a number of practical applications: At the meta-level, it can be decided if a (composite) metamodel characterizes a non-empty set of models, and a member can be automatically constructed. At the model-level, it can be decided if a submodel has an embedding in a well-formed model, and the larger model can be constructed. This amounts to automatic model construction from an incomplete model. We describe the concrete algorithms for constructively solving these problems, and provide concrete examples.

8. Ethan K. Jackson: The Model Integrated Computing Approach to Software Architecture , ASM 2007.
Download
abstract ::

Model-based design is an approach to software architecture that supports the rapid evaluation of many different design alternatives evolving from a high-level specification. Model integrated computing [1] (MIC) is one manifestation of model-based design, which relies on semantic units [2] and model transformations [3][4] to rapidly construct and evaluate various refinement paths. Abstract state machines are used at the core of MIC technologies to facilitate this goal. In this paper, we begin from the basic premises exemplified by abstract state machines, and show through examples, why the model-based approaches evolved and how they can be applied to today�s architectural challenges.

7. Ethan K. Jackson: The Software Engineering of Domain-Specific Model Languages: A Survey Through Examples , ISIS Technical Report, 2007.
Download
abstract ::

This paper presents the fundamental concepts of model-based design to the broader software engineering community. We examine model-based design from the perspective of domain-specific modeling languages (DSMLs). DSMLs capture the structure, behavioral characteristics, and abstractions of complex problem domains. Model transformations defined between language syntaxes serve as high-level specifications of domain-specific compilers. Additionally, transformations are used to change abstraction levels. This paper is example driven and includes examples from a number of tools including ASML [1], Ptolemy II [2], GME [3], and GReAT [4].

6. Ethan K. Jackson, and Janos Sztipanovits: Towards a Formal Foundation for Domain Specific Modeling Languages , EMSOFT 2006.
Download
abstract ::

Embedded system design is inherently domain specific and typically model driven. As a result, design methodologies like OMG�s model driven architecture (MDA) and model integrated computing (MIC) evolved to support domain specific modeling languages (DSMLs). The success of the DSML approach has encouraged work on the heterogeneous composition of DSMLs, model transformations between DSMLs, approximations of formal properties within DSMLs, and reuse of DSML semantics. However, in the effort to produce a mature design approach that can handle both the structural and behavioral semantics of embedded system design, many foundational issues concerning DSMLs have been overlooked. In this paper we present a formal foundation for DSMLs and for their construction within metamodeling frameworks. This foundation allows us to algorithmically decide if two DSMLs or metamodels are equivalent, if model transformations preserve properties, and if metamodeling frameworks have meta-metamodels. These results are key to building correct embedded systems with DSMLs.

5. Ethan K. Jackson, and Janos Sztipanovits: Correct-ed through Construction: A Model-based Approach to Embedded Systems Reality , ECBS 2006.
Download
abstract ::

We present a design methodology for specifying embedded systems that addresses the complex nature of embedded systems design. Our approach uses modern model-based techniques to correct specifications as they are constructed, driving the engineer towards a more correct specification. We also present a concrete specification language based on this methodology.

4. Kai Chen, Janos Sztipanovits, Sherif Abdelwalhed, and Ethan K. Jackson: Semantic Anchoring with Model Transformations , ECMDA 2005.
Download
abstract ::

Model-Integrated Computing (MIC) is an approach to Model-Driven Architecture (MDA), which has been developed primarily for embedded systems. MIC places strong emphasis on the use of domain-specific modeling languages (DSML-s) and model transformations. A metamodeling process facilitated by the Generic Modeling Environment (GME) tool suite enables the rapid and inexpensive development of DSML-s. However, the specification of semantics for DSML-s is still a hard problem. In order to simplify the DSML semantics, this paper discusses semantic anchoring, which is based on the transformational specification of semantics. Using a mathematical model, Abstract State Machine (ASM), as a common semantic framework, we have developed formal operational semantics for a set of basic models of computations, called semantic units. Semantic anchoring of DSML-s means the specification of model transformations between DSML-s (or aspects of complex DSML-s) and selected semantic units. The paper describes the semantic anchoring process using the meta-programmable MIC tool suite.

3. Ethan K. Jackson, and Janos Sztipanovits: Using Separation of Concerns for Embedded Systems Design , EMSOFT 2005.
Download
abstract ::

Embedded systems are commonly abstracted as collections of interacting components. This perspective has lead to the insight that component behaviors can be defined separately from admissible component interactions. We show that this separation of concerns does not imply that component behaviors can be defined in isolation from their envisioned interaction models. We argue that a type of behavior/interaction co-design must be employed to successfully leverage the separation of these concerns. We present formal techniques for accomplishing this co-design and describe tools that implement these formalisms.

2. Mark Kahrs, Steven P. Levitan, Donald M. Chiarulli, Timothy P. Kurzweg, Jose A. Martinez, Jason Boles, Ahijhit J. Davare, Ethan K. Jackson, Craig Windish, Fouad Kiamilev, Amit Bhaduri, Muhammad Taufik, Xingle Wang, Arthur S. Morris, James Kruchowski, and Barry K. Gilbert: System-level modeling and Simulation of the 10G optoelectronic interconnect , Journal of Lightwave Technology, 2003.
Download
abstract ::

Mixed-signal multidomain systems present a challenge for computer-aided design tools. Optical and electronic simulation tools are available as separate entities. However, to date, successful system-level cosimulation has not been implemented, leading to expensive refabrication. We present a unique system-level simulation tool for mixed electrooptical systems. We apply our tool Chatoyant to the simulation of an optical high-speed free-space interconnect system designed for 10-GHz speeds. The 10G free-space optical interconnect module has optical, optoelectronic, and microwave components and thus is an ideal vehicle to use as a test system. We demonstrate how Chatoyant, a mixed-signal multidomain simulator, has been used to evaluate end-to-end performance of this complex system, including the exploration of design tradeoffs and mechanical tolerancing.

1. Mark Kahrs, Steven P. Levitan, Donald M. Chiarulli, Timothy P. Kurzweg, Jose A. Martinez, Jason Boles, Ahijhit J. Davare, Ethan K. Jackson, Craig Windish, Fouad Kiamilev, Amit Bhaduri, Muhammad Taufik, Xingle Wang, Arthur S. Morris, Joseph Repke, James Kruchowski, and Barry K. Gilbert: Signal Integrity Evaluation of a 10 Gbits/sec Optoelectronic Interconnect , Microwave Symposium Digest, 2003.
Download
abstract ::

Signal integrity is of vital importance to high speed interconnects. The 10G system is a 10 Gbit/second optical interconnect with a cross-section bandwidth of over 1T bit/second fabricated on a heterogeneous platform consisting of a multi-chip module, high-speed SiGe and GaAs opto-electronics. We compare lumped and multisegment microstrip models of the transmission lines on the MCM hybrid. We also model the wirebonds using a quasi-static model and a Co-Planar Waveguide (CPW) model for the bump bonds between the GaAs and SiGe substrates. These models are utilized by a behavioral simulator to demonstrate the effects of interconnect components on waveform shape. The results demonstrate convincingly that signal integrity is of critical importance to end-to-end performance measures at high transmission speeds and that incorporating these models is important to behavioral simulation.

 > People > Ethan Jackson