Formal Techniques for Design and Development of Safety Critical Embedded Systems from Polychronous Models

Simple item page
dc.contributor.authorNanjundappa, Maheshen
dc.contributor.committeechairShukla, Sandeep K.en
dc.contributor.committeememberHaghighat, Alirezaen
dc.contributor.committeememberWang, Chaoen
dc.contributor.committeememberClancy, Thomas Charles IIIen
dc.contributor.committeememberMili, Lamine M.en
dc.contributor.departmentElectrical and Computer Engineeringen
dc.date.accessioned2016-11-19T07:00:18Zen
dc.date.available2016-11-19T07:00:18Zen
dc.date.issued2015-05-28en
dc.description.abstractFormally-based design and implementation techniques for complex safety-critical embedded systems are required not only to handle the complexity, but also to provide correctness guarantees. Traditional design approaches struggle to cope with complexity, and they generally require extensive testing to guarantee correctness. As the designs get larger and more complex, traditional approaches face many limitations. An alternate design approach is to adopt a "correct-by-construction" paradigm and synthesize the desired hardware and software from the high-level descriptions expressed using one of the many formal modeling languages. Since these languages are equipped with formal semantics, formally-based tools can be employed for various analysis. In this dissertation, we adopt one such formal modeling language - MRICDF (Multi-Rate Instantaneous Channel-connected Data Flow). MRICDF is a graphical, declarative, polychronous modeling language, with a formalism that allows the modeler to easily describe multi-clocked systems without the necessity of global clock. Unnecessary synchronizations among concurrent computation entities can be avoided using a polychronous language such as MRICDF. We have explored a Boolean theory-based techniques for synthesizing multi-threaded/concurrent code and extended the technique to improve the performance of synthesized multi-threaded code. We also explored synthesizing ASIPs (Application Specific Instruction Set Processors) from MRICDF models. Further, we have developed formal techniques to identify constructive causality in polychronous models. We have also developed SMT (Satisfiablity Modulo Theory)-based techniques to identify dimensional inconsistencies and to perform value-range analysis of polychronous models.en
dc.description.degreePh. D.en
dc.format.mediumETDen
dc.identifier.othervt_gsexam:5386en
dc.identifier.urihttp://hdl.handle.net/10919/73483en
dc.publisherVirginia Techen
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subjectModel-based Designen
dc.subjectMBDen
dc.subjectSoftware Synthesisen
dc.subjectFormal techniquesen
dc.subjectCode generationen
dc.subjectFormal analysisen
dc.titleFormal Techniques for Design and Development of Safety Critical Embedded Systems from Polychronous Modelsen
dc.typeDissertationen
thesis.degree.disciplineComputer Engineeringen
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen
thesis.degree.leveldoctoralen
thesis.degree.namePh. D.en

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Nanjundappa_M_D_2015.pdf
Size:
3.73 MB
Format:
Adobe Portable Document Format
Download

Collections

Doctoral Dissertations