Trustworthy smart city systems using refinement and Event-B Theories

Abstract

Smart city systems do not only handle information but also handle many critical aspects of citizens’ lives, including automobiles, healthcare, banking, etc. Smart city systems need to be both safe and secure systems. Therefore, this paper uses formal methods to develop safe and secure systes for smart city. However, because the creation of formal models is considered a difficult task that requires experience in modeling and a strong mathematical background, many techniques and patterns should be introduced to simplify the construction of formal models to make them more accessible for the development of systems, especially for systems pertaining to smart city services. In this paper, we propose an approach that uses Event-B theories to support data refinement and reduce the burden of proof for constructing Event-B formal models based on reused modeling components. In particular, we develop Event-B theories for common data structures based on pointers that could be used as patterns to carry out the refinement of abstract data structures, such as sets, lists and sequences. These data structures can offer solutions for the management of smart city services. We applied the proposed approach to construct Event-B models for task lists in a real-time operating system (FreeRTOS) to evaluate our approach. We successfully were able to model five task lists in FreeRTOS and developing data refinement levels without the need of spending long time in modeling or re-carrying any proofs.