A joint project of the Graduate School, Peabody College, and the Jean & Alexander Heard Library

Title page for ETD etd-04082011-145057

Type of Document Dissertation
Author Balasubramanian, Daniel Allen
URN etd-04082011-145057
Title Behavioral Semantics of Modeling Languages: A Pragmatic Approach
Degree PhD
Department Computer Science
Advisory Committee
Advisor Name Title
Gabor Karsai Committee Chair
  • formal methods
  • model-based development
  • Domain-specific languages
Date of Defense 2011-03-25
Availability unrestricted
Domain-specific modeling languages (DSMLs) are specialized languages tailored with concepts and features of a particular domain. The abstractions offered by DSMLs allow designers of software systems to ignore implementation details and instead focus on the system at a high level. While higher levels of abstraction can offer many advantages, there are still unresolved issues with DSMLs. One of these is the difficulty of applying formal verification methods.

This dissertation presents two contributions that assist with the formal verification of domain-specific models. The first is a unified framework in which Statechart models of different semantic variants can be defined, simulated and verified. The key idea is that the user describes only the structure of a model, and then selects the semantics from a set of pluggable components. This allows a single model to be executed using multiple semantics, and a system comprised of interacting models using different semantics can be simulated and verified in a single environment. A lightweight method for specifying properties based on a pattern system was also developed. To perform analysis, the framework is integrated with Java Pathfinder, a software model checker, and Symbolic Pathfinder, its symbolic execution engine. Symbolic execution allows both test-vector generation and reachability analysis.

The second major contribution is an extension to Formula, a modeling language and analysis tool from Microsoft Research, that calculates execution traces of models. The behavioral semantics are defined as a set of model transformations, each of which represents an atomic step of execution. The trace computing extension consists of three components. The first is a component that applies all applicable transformations to an input model at a given step and creates a separate trace for each application. The second component is used to create a separate trace for each non-deterministic choice of the input parameters that are passed to a transformation, making non-determinism inside a single execution step explicit to the trace computing module. The third component stores execution traces efficiently by computing and storing only the differences between consecutive steps in a trace when possible.

  Filename       Size       Approximate Download Time (Hours:Minutes:Seconds) 
 28.8 Modem   56K Modem   ISDN (64 Kb)   ISDN (128 Kb)   Higher-speed Access 
  DanielDissertation.pdf 5.93 Mb 00:27:26 00:14:07 00:12:21 00:06:10 00:00:31

Browse All Available ETDs by ( Author | Department )

If you have more questions or technical problems, please Contact LITS.