Dewan Mohammad Moksedul Alam
School of Computing and Information Sciences
Dewan Mohammad Moksedul Alam is a Ph.D. candidate in the School of Computing and Information Sciences at Florida International University under the supervision of professor Xudong He. His research interests lie within formal methods of software engineering, model-driven development, automation in software development, testing, code generation, etc. He completed his B.Sc. in computer science from Bangladesh University of Engineering and Technology in January 2008. Before joining FIU in Fall 2015, he has been working as a Senior Software Engineer in companies like Escenic/Vizrt, Cefalo AS and lead several Scrum teams to successful completion of many software components. He also has contributions to several open-source tools for automation and productivity.
Cyber-Physical Systems (CPSs) are an ecosystem of heterogeneous components where physical devices controlled by digital controllers come together towards the accomplishment of some specific goals. In recent years they have become ubiquitous. From utility features in household devices to safety-critical features in cars, trains, aircraft, robots, smart healthcare devices they are being used. Designing CPSs and their controller algorithms are extremely challenging due to the interaction of heterogeneous, multidomain, and physical systems. At the same time, it is crucial that they work correctly since we rely on CPSs for safety-critical tasks. In recent decades, several methodologies and tools have been proposed for this purpose. Reachability analysis is one of the effective methods to analyze CPSs. Many efficient algorithms and sophisticated tools are developed to perform reachability analysis using Hybrid Automata.
High-level Petri nets, a powerful formal method to model and nalyze distributed, concurrent systems, have been being studied and used in the industrial level for decades. But there are not many tools and methods available to utilize it to model and analyze CPSs. In this work, a methodology is presented to combine the modeling power of Predicate Transition Nets (PrTN), a class of high-level Petri nets, and state of the art analysis techniques for CPSs. First, a methodology is provided to model CPSs using Hybrid Predicate Transition Nets (HPrTN), an extension to PrTN. Then, a translation-based analysis technique is provided to transform HPrTN models to the input language of a sophisticated reachability analysis tool SpaceEx. It is one of the states of the are reachability analysis tools for hybrid systems with non-linear affine dynamics. Some benchmark CPSs are studied to compare the performance of the analysis of these converted models.