Design and verification of a mobile robot based on the integrated model of cyber-Physical systems

The paper describes the new model, which is a key element of the design and verification methodology for secure cyber-physical systems. The proposed model represents cyber-physical systems as a set of building blocks with properties and connections between them, while each building block is the projection of the integrated model. The models of attacker and attack actions are an external models that are connected with an integrated model: attack actions impact is modelled through changes in the properties of the system or its elements while the number of possible attack actions is reduced according to the attacker possibilities. The novelty of the proposed model lies in the strong focus on security and possibilities of direct (from the projections to the integrated model) and reverse (from the integrated model to the projections) transformations. Verification process is an integral part of the proposed solution. Verification provides the formal check of the system creation possibility in accordance with the requirements and limitations as well as that designed system is secured against an attacker of certain level of knowledge which is connected from certain access point and has certain amount of resources. During the experiments SPASS theorem prover, the Maude system and daTac were used. As an example of the proposed model application, firstly, an access control system was considered. This system contains Arduino microcontrollers, software agents, web-servers and different sensors. To provide an additional example an use case about mobile robot for perimeter monitoring was also presented. For the experiments, it was decided to use the LEGO 9797 Mindstorms NXT.