Morse Reseach group

CHECKIT: New Extensions of Formal Methods in Modelling, Verification, Synthesis and Optimization of Embedded and Mobile Communication Systems: Application of Certification of LTE Protocols

Computer systems are gradually replacing tasks that due to its critical nature have been conducted manually. This explosion of new applications has been possible thanks to the improvement of hardware devices that eventually automate processes, and the development of the software industry that has produced new intermediate and high level programming technologies, with a much greater expressive power, able to solve problems of great magnitude.

Simultaneous with this growth in demand for software services, we have developed the so-called formal techniques that aim to improve the quality and reliability of the software that is provided to the user. These techniques make use of mathematical language to minimize the number of errors, ensuring that the software meets a set of properties that are considered critical to its scope. Although initially, the use of formal techniques was criticized for its dubious practical application, today, its use is widely accepted, so that the development of any product is usually accompanied by his modeling and / or analysis by any formal technique. This is due mainly to the development of modeling techniques and powerful analysis and tools that support these techniques and have been proven extensively its usefulness in practice.

Perhaps the method known as model checking is the most influential in the progressive integration of formal techniques in software development, software fundamentally concurrent or distributed. The ubiquity of model checking and its apparent success at industrial level is because a balanced way mathematical formalization, and properties of both software system to be analyzed, and practicality, since the model checking is an algorithmic technique aimed at building tools to carry out automatically the complex task of software verification.

The current trend in the formal techniques area is thus finding new formalism, or extension of existing, considering different aspects of the software that classically have not been considered. For example, most of the systems listed in the real world are not completely discrete but have some component, usually associated with a physical device which acts continuously. Such systems are called hybrids, and are characterized at times behave discreetly, while in others, evolve through continuous dynamics (uncountable). Another interesting aspect of real systems is that in many instances, have a random behavior, so that incorporate some uncertainty parameter, having a function that defines probabilistic evolution. To model and analyze hybrid and / or probabilistic systems, it is necessary to incorporate new techniques in formal parameters that refer to these aspects.

Although the main applications of the techniques are formal modeling and verification, it can be found that in new fields demonstrated its usefulness. Specifically, the problem ofautomated synthesis may be approached from the standpoint of formal techniques. For example, the model checking techniques can be seen as an automated and exhaustive search method of states that satisfy a property which can be interpreted as a target. In this case, the formal techniques can provide new solutions to problems, such as thecontrolled synthesis and optimization have been addressed from other perspectives. Along the same lines, the emergence of new software application scenarios, such as the aforementioned automated component adaptation, in the context of software services can be solved by using standard not existing formal techniques, or defining new formal frameworks allow the construction of software adapters correct.

This project has two technical objectives. On the one hand, improve software quality, which may contain continuous components, and uncertainties, extending the model checking technique appropriately: by defining new modeling languages, which are able to describe the new features, using the extension of model checking algorithms, to take into account the continuous and probability, and by extending existing model checking tools to implement these proposals.

On the other hand, the second technical objective is the study of new non-standard applications of model checking in the context of the synthesis and optimization of software drivers and adapters, as well as the development of new formal frameworks that solve the problem of dynamic adaptation software for correct reception of services by users.

This project is proposed as a driving project whose relevance to Andalusian industrial sector is evidenced by the letters of support from companies that are attached to the document. The company AT4 wireless will work on the project in the form of subcontracting to develop part of the certification infrastructure services and protocols for LTE networks. The company ADIF (Railway Infrastructure Administrator) will monitor the work on railway control systems and provide the group using their TIC Railway Technology Center of Malaga. The company NOVASOFT is interested in the developments relating to the dynamic generation of service adapters. And the companyVodafone will track the results in the field of mobile telephony.