The choice of an adequate notation and subsequent system formalization are the crucial points for the design of cyber-physical systems (CPSs).Here, an appropriate notation allows an explicit specification of the deterministic system behavior for specified initial states and inputs.We base our study on an industrial example (water tank) that comprises nominal as well as safety-critical states, and focus on the notation's support to validate/verify crucial safety properties.Several industrial notations (e.g.Matlab/Simulink © ) to design and simulate such a hybrid system have been tried based on our physical model.In addition, we remodel our example using the well-founded mathematical formalism of hybrid automata.It enables us to formally express and verify important safety properties using the theorem prover KeYmaera.This work was supported by the

Building robust software can be considered a major challenge in current software engineering processes. This task is especially relevant for the code of cyber-physical systems (CPS) that interact with tangible data of the environment and make decisions that have an impact on the real world. The study of good practices of the architectural organization of such software systems is suitable to conduct on solutions with open-source code, which are developed by large communities of enthusiasts. Such a code bears a long history and has been tested many times on real devices in a real-world environment. The construction of various models using the program code allows us to understand stable architectural solutions, to present them in a graphical form; these solutions can be used in STEM centers when designing other systems, taking into account all the achievements of the communities. In addition, it is possible to propose methods for analyzing models to prove various properties of cyber-physical systems. In this paper, we analyze ArduPilot Mega (APM), an Arduino-compatible solution for building DIY driving and flying systems. The solution is based on a specially designed board with a controller and necessary peripherals, as well as a firmware code in a C++ -compatible dialect. Since there are many limitations associated with hardware, it is advisable to carry out a so-called co-modeling, taking into account both hardware and software sides. We consider modeling the interaction of equipment on connected pins and data transmission buses, the software part in the form of a class diagram for the solution. We then describe methods for analyzing the interactions between tasks running on the system through shared variables and evaluating the performance of the task scheduler.