What do I want to achieve?
At the beginning of the 21.st century human race is facing The Third Industrial Revolution. We are gonna build smart self-driving cars, smart homes, smart agriculture and all these things will be full of sensors and controllers. These devices will be combining physical world with the world of software. Such devices are called cyber-physical systems. They will monitor the environment around us in real time and react on changes by changing their behaviour. We are gonna use such devices (e.g. self-driving cars) for our everyday life hence they have to be as secure as possible. If the whole population should use such cyber-physical systems, it has to be even more secure than Elon's Musk SpaceX rockets.
How do I want to achieve it?
So how one can improve safety of such complex systems like smart cars, trains, wind turbines? To answer such question we have to ask another one. How do we build these things? How do we test them and how do we measure their safety? Companies nowadays first create a model of a new device before they actually manufacture it. They call it a Model-Based Design. It actually makes sense, creating model in MATLAB/Simulink is much easier and cheaper than manufacturing it in real life. For example you got a genious idea of creating a square wheel. Very innovative. But since you have no proof it will actually work in real life (which it won't, let me tell you), it is smart to create a digital model first prior to the manufacturing process. Then you can run a simulation and see how poorly your square wheel operates. So we build new things by modeling them first in a digital world and running simulations. If that looks good, we can create a prototype and test it in the real life. I specialize on those models that you create.
People make mistakes. When an engineer creates a model of a brand new space rocket in a shape of a carrot, he will probably miscalculate something. We do not want these mistakes to propagate all the way down to the prototype. Especially when you are building a 100 million $ rocket. In order to avoid this companies do test each model against a set of requirements. Falsification they call it. Such requirements can be of all sorts. For example Requirement n.1: Carrot Space Rocket must never enter the state when there would be 10 g-force, because that is deadly for human beings. Now if we have a model of a Carrot Space Rocket, we can run a simulation of it's launch and observe if it would violate our requirement number one and thus kill all crew.
Run these tests manually is very, very, VERY time-consuming. That is why we have tools to automate them (e.g. S-TaLiRo, Modelica, or Ptolemy). Sadly these tools have it's limitations, since they treat most of the models as black-box. When dealing with models of smart systems (such as Anti-lock braking system in cars) these tools cannot effectively verify that model meets the requirements. This combination of discrete logic and continuous behaviour of mechanical parts makes the verification process very hard. And what I do is that I try to invent new epic algorithms that would deal with such complexity.
Tools I work with
But before inventing anything new, first one has to get acquainted with the tools that are generally used in the area of falsification of models. The cornerstone of working with digital models is MATLAB & Simulink. Using these two tools we can create models of devices such as DC-motor controller. MATLAB & Simulink can be used to model continuous systems That is nice, but cyber-physical systems contain both parts, continuous and discrete. To add the discrete part we can use downloadable toolbox called StateFlow.