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

Title page for ETD etd-12122013-150348

Type of Document Master's Thesis
Author Agrawal, Akshay
Author's Email Address akshay.agrawal@vanderbilt.edu
URN etd-12122013-150348
Title Model-based verification toolchain for increasing trust on automated code-generators
Degree Master of Science
Department Computer Science
Advisory Committee
Advisor Name Title
Dr. Joseph Porter Committee Member
Dr. Sandeep Neema Committee Member
  • Model-Based Design
  • Code-Generator
  • Cyber-Physical Systems
Date of Defense 2013-12-09
Availability unrestricted
Automated code-generators are increasingly becoming the workhorses in model-based development of Cyber-Physical Systems (CPS). Significant model-driven tools have emerged incorporating advanced model-checking methods that can provide some assurance regarding the quality and correctness of the models. However, the code generated from these models still remains circumspect, since the correctness of the code-generators cannot be assumed as a given. Therefore, to increase trust in the code-generators formal verification of their correctness is paramount. Manual verification of entire code-generators under all possible context and inputs is a daunting task, considering the complexity and size of code-generators. We are proposing a pragmatic approach for ascertaining correctness of code-generators that, instead of verifying their explicit implementation, verifies the correctness of the generated code with respect to a specific set of user-defined properties to establish that the code-generators are property-preserving.

In this thesis, we discuss an existing model-based design method for compositional synthesis of CPS and show the integration of a toolchain with it, which provisions an automated verification workflow for proving correctness of the code generated by code-generators in an iterative fashion. In order to make the verification workflow conducive to domain engineers, who are not often trained in formal methods, we include a mechanism for high-level specification of temporal properties using pattern-based verification templates. The presented toolchain leverages state-of-the-art verification tools. We illustrate the approach of presented toolchain with a case-study of an Ignition Logic Controller of an automotive vehicle.

  Filename       Size       Approximate Download Time (Hours:Minutes:Seconds) 
 28.8 Modem   56K Modem   ISDN (64 Kb)   ISDN (128 Kb)   Higher-speed Access 
  Agrawal.pdf 5.60 Mb 00:25:55 00:13:20 00:11:40 00:05:50 00:00:29

Browse All Available ETDs by ( Author | Department )

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