Formalization and Certification of Software for Smart Cities

The amount of available urban data has been increasing over the last years which leaded to new research challenges on Smart Cities domain. Verifying and certifying systems in this domain is one of the challenges that still require some effort. Smart Cities models may be seen as Cyber-Physical Systems and they may be formalized as Finite State machines. Logic-based systems makes possible to take advantage of a wide framework for formally verify this domain. Proof assistants are logic based computational tools developed to mechanize the construction of proofs and Coq, among others, plays an essential role in software validation. This work is tailored to show a way to reason over these models as Finite State machines formalized in the Coq proof assistant from which it is possible to provide certified software to the Smart Cities domain.