Title page for ETD etd-08112011-161349


Type of Document Dissertation
Author Jose, Bijoy Antony
Author's Email Address bijoyaj@vt.edu
URN etd-08112011-161349
Title Formal Model Driven Software Synthesis for Embedded Systems
Degree PhD
Department Electrical and Computer Engineering
Advisory Committee
Advisor Name Title
Shukla, Sandeep K. Committee Chair
Abbott, A. Lynn Committee Member
Hsiao, Michael S. Committee Member
Schaumont, Patrick Robert Committee Member
Vullikanti, Anil Kumar S. Committee Member
Keywords
  • synchronous systems
  • Model driven code generation
  • software synthesis
  • multi-threading
  • polychronous formalism
Date of Defense 2011-08-02
Availability unrestricted
Abstract
Due to the ever increasing complexity of safety-critical applications, handwritten code is being

replaced by automatically generated code derived from a high level specification. Code generation

from high level specification requires a model of computation with an underlying formalism

and correctness-preserving refinement steps to generate the lower level application code. Such

software synthesis techniques are said to be ‘correct-by-construction’. Synchronous programming

languages such as Esterel, LUSTRE, which are based on a synchronous model of computation

are used for sequential code generation. They work on a synchrony assumption (zero time intraprocess

computation and zero time inter process communication) at the specification level. Early

versions of synchronous languages followed an execution pattern where an iteration of software

was mapped to an interval between ticks of an external reference clock. Since this external reference

tick was unrelated to variables (or signals) within the software, redundant operations such

as reading of ports, computation of guards were performed for each tick. In this dissertation, we

highlight some of these performance issues and missed optimization opportunities. Also we show

how a multi-clock (or polychronous) formalism, where each variable has an independent rate of

execution associated with it, can avoid these problems.

An existing polychronous language named SIGNAL, creates a hierarchy of clocks based on the

rate of execution of individual variables, to form a root clock which acts a reference tick. We

seek to replace the clock analysis with a technique to form a unique order of events without a

reference time line. For this purpose, we present a new polychronous formalism termed Multi-rate

Instantaneous Channel connected Data Flow (MRICDF). Our new synthesis technique inspects

the specification to identify a master trigger at a Boolean equation level to act as the reference

tick. Furthermore, we attempt to make polychronous specification based software synthesis more

accessible to practicing engineers, by constructing a software tool EmCodeSyn, with a visual environment

for specification and a more intuitive analysis technique. Our Boolean approach to

sequential synthesis of embedded software has multiple implementations, each of which utilizes

existing academic software tools. Optimizations are proposed to minimize synthesis time by simplifying

the input to these external tools. Weaknesses in causal loop analysis techniques applied

by existing synthesis tools are highlighted and solutions for performing time efficient loop analysis

are integrated into EmCodeSyn. We have also determined that a part of the non-synthesizable

polychronous specifications can be used to generate correct multi-threaded code. Additionally,

we investigate composition of polychronous modules and propose properties that are necessary to

guarantee agreement on shared signals.

Files
  Filename       Size       Approximate Download Time (Hours:Minutes:Seconds) 
 
 28.8 Modem   56K Modem   ISDN (64 Kb)   ISDN (128 Kb)   Higher-speed Access 
  Jose_BA_D_2011.pdf 2.00 Mb 00:09:15 00:04:45 00:04:10 00:02:05 00:00:10

Browse All Available ETDs by ( Author | Department )

dla home
etds imagebase journals news ereserve special collections
virgnia tech home contact dla university libraries

If you have questions or technical problems, please Contact DLA.