10:30 AM - 12:30 PM on Wednesday, May 28, 2014
Location: Arlington 5-024
M.S., Thesis, Defense for Safa Messaoud
Graduate Advisory Committee:
Dr. Sandeep K. Shukla, Chair
Dr. Michael S. Hsiao
Dr. JoAnn Mary Paul
As Cyber Physical Systems (CPS) are getting more complex and safety critical, Model Based Design (MBD), which consists of building formal models of a system in order to be used in verication and correct-by-construction code generation, is becoming a promising method- ology for the development of the embedded software of such systems. This design paradigm signicantly reduces the development cost and time while guaranteeing better robustness, capability and correctness with respect to the original specications, when compared with the traditional ad-hoc design methods. SIMULINK has been the most popular tool for em- bedded control design in research as well as in industry, for the last decades. As SIMULINK does not have formal semantics, the application of the model based design methodology and tools to its models is very limited. In this thesis, we present a semantic translator that trans- form discrete time SIMULINK models into SIGNAL programs. The choice of SIGNAL is motivated by its polychronous formalism that enhances hat enhances synchronous program- ming with asynchronous concurrency, as well as, by the ability of its compiler of generating deterministic multi-thread code. Our translation involves three major steps: clock inference, type inference and hierarchical top-down translation. We validate the semantic preservation of our prototype tool by testing it on different SIMULINK models.