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, aircrafts, 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 and theorem proving are some effective methods to analyze CPSs. Hybrid Automata and Dynamic Differential Logic are some modeling tools in the focus of recent research to apply these methods.
High-level Petri nets, a powerful formal method to model and analyze 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, we present a methodology 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, we provide a methodology to model CPSs using Hybrid Predicate Transition Nets (HPrTN), an extension to PrTN. Then, we provide model translators to transform HPrTN models into Hybrid Automata and Differential dynamic logic. The hybrid automata will be used in the tool SpaceEx for reachability analysis and differential dynamic logic will be used with a theorem prover KeYmaera X to find proof of the safety properties of the HPrTN models.