Model to code generation of UML/SysML activity diagrams for ARM CortexM MCUs (Master Thesis):

2013-2015 Hardware Verification Group ARM Cortex-M SysML Formal Verification Model Checking

Previously in our group, we formalized SysML activity diagrams by developing a calculus called New Activity Calculus (NuAC). In this work, we redefined NuAC terms to support RTX (Keil Real-Time Operating System) and present an automated SysML/UML activity diagram to RTX code generator, using mapping rules expressed in NuAC. To achieve this goal, we proposed a set of rules that were used for mapping a SysML/ UML activity diagram into a suitable code to be executed on ARM CortexM processor family. To automate the process of code generation, we developed a JAVA application that uses the proposed rules to automatically generate the RTX code from the input activity diagram model.

Synthesis and Verification of Data Encryption Standard:

Summer 2013 Formal Hardware Verification Synthesis

The aim of this project was to answer the following: Given a behavioural (as a reference) and a netlist of a design, using equivalency checking, find the bugs that resides in the netlist. We first started by describing the functional behavior and specification of a Data Encryption Standard(DES). We then synthesized the provided behavioral code (HDL) in Synopsys Design Compiler and we discussed about the synthesis results. The generated net list from the synthesizer was used as our reference design. We applied equivalency checking techniques on the given netlist (buggy) and reference design to find bugs. Furthermore, we introduced and explained the techniques that we used for finding bugs in the design. Finally, a comparison between Synopsys Formality and Cadence Conformal was described.

Schematic view of both reference and implementation circuits illustrating the bug in implementation.

Formal Modeling, Verification and Implementation of a Train Control System:

Winter 2015 ARM-CortexM4 Formal Verification Model checking AutoFOUS3 (AF3) Python

In this project the BART train control system was formally modeled and after verifing the properties of the system, the train control algorithm was then implemented on an ARM Cortex-M4 processor. We first started by formally modelling the train operation and its control system. To verify the correct functionality of the algorithm, we expressed the model in AF3 block representation. Using NuSMV, we verified the essential properties of the system. Finally, the BART’s train control system was implemented on an ARM platform.