Formal Specification Of Safety Critical Mobile Applications

Mobile Computing paradigm has been applying to an ever more large set of applications including banking, transportation and healthcare, which present critical requirements from the point of view of functional correctness, reliability, availability, security and safety. Differently from the case of classical safety critical applications for which software engineering has developed several formal methods and methodologies in order to specify, validate and verify system software requirements, in the case of mobile systems classic methods can not be applied as they are because of two main reasons: mobile applications are error prone and classic formal methods (eg. finite state machines, labeled transition systems, Petri-nets, timed automata, pi-calculus, process algebra, etc.) do not take into account the most remarkable concepts involved in mobile applications, that are location and mobility of people, code and resources.