The relationship between states (status of a system) and modes (capabilities of a system) used to describe system requirements is often poorly defined. The unclear relationship could make systems of interest out of control because of the out of boundaries of the systems caused by the newly added modes. Formally modeling and verifying requirements can clarify the relationship, making the system safer. To this end, an innovative approach to analyzing requirements is proposed. The MoSt language (a Domain Specific Language implemented on the Xtext framework) is firstly designed for requirements modeling and a model validator is realized to check requirements statically. A code generator is then provided to realize the automatic model transformation from the MoSt model to a NuSMV model, laying the foundation for the dynamic checks of requirements through symbolic model checking. Next, a NuSMV runner is designed to connect the NuSMV with the validator to automate the whole dynamic checks. The grammar, the model validator, the code generator, and the NuSMV runner are finally integrated into a publicly available Eclipse-based tool. Two case studies have been employed to illustrate the feasibility of our approach. For each case study, we injected 14 errors. The results show that the static and dynamic checks can successfully detect all the errors.

This paper addresses the issue of formal verification of ethical choices in Industrial Cyber-Physical Systems. An innovative approach based on Beliefs, Desires, and Intentions (BDI) agents and model checking is proposed. To do so, we first give a formal definition of ethical rules. Based on this definition, an algorithm is then designed to implement ethical reasoning. Finally, we apply this approach to TRACILOGIS (an academic full-sized application platform) to illustrate its feasibility. Four properties are designed and checked. The verification results show the agent with ethics can always reason out the least unethical actions to take.