Facing the challenges that software systems pose today requires innovative smart solutions. Many challenges in Information Technology for the Digital Society involve the analysis of complex systems, e.g., scheduling problems in a smart factory, resource and security analysis in distributed systems, safety and liveness concerns in multi-threaded programs or dynamic resource allocation in a cloud system, among others. Such complex interdependent systems are growing in smart cities, the healthcare industry, or sustainable transport. Most of these systems are safety critical and economically vital. However, building robust tools to analyze them still remains a major endeavour. Our approach follows the next three steps: first, a real complex system is modeled using a more abstract representation; second, smart solutions are obtained by expressing the problems in some logical framework; and then, finally, powerful logic-based technologies are applied to analyze and/or solve the problems. The LoBaSS project contributes in all three directions: modeling real problems, finding representations in some appropriate logical framework, and developing tools and techniques to better solve or optimize the resulting problems. This overall approach allows us to apply the same techniques in multiple application domains (e.g., cloud computing, smart factories, protocol analysis), which makes the development of tools to solve hard real problems significantly easier and faster. As logical frameworks we are mainly using extensions and combinations of propositional and first-order logic and algebraic structures. In particular, we are considering: SAT (satisfaction of propositional formulas), SAT modulo theories (SMT, where propositions are replaced by atoms in a given theory), Constraint Programming (CP, where clauses are replaced by predicates over a pre-defined language), Fuzzy Logic (FL, where clauses have some uncertainty), Rewrite Logic (RWL, with modelling and programming advanced capabilities), Logic Programming (LP), Fuzzy Logic Programming (FLP) and Abstract Interpretation (AI, based on monotonic functions over lattices). In this project we will focus on the combination and extension of these successful formal languages to get the necessary expressiveness for our practical applications. Today's challenges in Information Technology will guide our work in scheduling and planning, security, machine learning, complex systems analysis, bio-informatics or XML manipulation, developing efficient algorithms and tools to solve them. As specific application domains we consider: (a) sports scheduling as done with KNVB, (b) optimization and planning in collaboration with Barcelogic Solutions and with the interest of companies like SIMO and E2F, (c) analysis of complex systems in collaboration with Microsoft Research and with the interest of many national and international companies (IBM, Thales, Clearsy, Vossloh, Edicom and Semantic Systems), (d) security in collaboration with the University of Illinois and the Naval Research Laboratory, (e) fuzzy scheduling for resource usage within cloud data centers with the Umea University and (f) analysis of transcript sequences in collaboration with the IMIM. All in all, our project covers all the way in the development and application of computer technologies from the basic theory and techniques to the current challenges of information technologies in the digital society and the smart, green and integrated transport.
Plan Estatal de Investigación Científica y Técnica y de Innovación 2013-2016
Programa Estatal de I+D+i Orientada a los Retos de la Sociedad
Retos de Investigación: Proyectos de I+D+i
Gobierno De España. Ministerio De Economía Y Competitividad, Mineco