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

Formally-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.

Name thesis:degree_name

Ph. D.

Level thesis:degree_level

doctoral

Discipline thesis:degree_discipline

Computer Engineering

Department dc:contributor.department

Electrical and Computer Engineering

Grantor dc:publisher

Virginia Tech

Year dc:date.issued

2015

Author dc:creator

• Nanjundappa, Mahesh

Chair dc:contributor.committeechair

• Shukla, Sandeep K.

Committee members dc:contributor.committeemember

• Haghighat, Alireza
• Wang, Chao
• Clancy, Thomas Charles III
• Mili, Lamine M.

• Model-based Design
• MBD
• Software Synthesis
• Formal techniques
• Code generation
• Formal analysis

Statement dc:rights

• In Copyright

Licence dc:rights.uri

• http://rightsstatements.org/vocab/InC/1.0/

Dc Identifier Other

vt_gsexam:5386

OAI identifier oai:identifier

oai:vtechworks.lib.vt.edu:10919/73483