Workshop

LfSA 2012 - Logics for System Analysis

Berkeley, July 7, 2012

Workshop affiliated with CAV

News: Invited Speakers Confirmed

have been confirmed as invited speakers for LfSA'12.

Overview

Safety-critical systems occur in various different forms like real-time systems, embedded systems, hybrid systems, distributed systems, and cyber-physical systems. They are becoming more and more important in application domains, including aviation, automotive, railway, robotic, or medical applications, where both safety and security are relevant aspects. To ensure the correct functioning of safety-critical systems, it is necessary to model and verify aspects of hardware (including physical properties or movement), software, communication, and qualitative and quantitative aspects of the system environment. Especially, the role of the system environment is becoming crucial for faithful system analysis. Classical computer analysis and verification mostly ignores the computer environment, is abstract with respect to the passing of real time, and has no notion of space, with the possible exception of communication distance. The interfacing with physical processes in modern safety-critical systems requires rethinking the foundations of system analysis.

Logics for system analysis, system modeling, and specification, are primary tools to analyze system behavior. Logic is equally important for understanding the theoretical foundations of system analysis and verification and serves as the basis for practical analysis tools that establish correct functioning of systems or find bugs in their designs. Depending on the nature of the system, modeling languages that are amenable to logical analysis and the study of correctness properties could include logical representations, automata, state charts, Petri nets, dataflow models, or systems of differential equations. Several system models can be analyzed rigorously with the help of techniques like logical calculi, decision procedures, model checking, and abstraction.

This workshop is devoted to the systematic theoretical study, practical development, and applied use of logics for system analysis and verification. The purpose of the LfSA workshop is to bring together researchers and practitioners interested in studying practically relevant systems or in developing the logical foundations and analysis tools for their study. With the increasing involvement of multiple aspects of safety-criticality, a common venue to share and discuss results is becoming invaluable for promoting collaboration and dissemination of new ideas among scientists with theoretical interests, practitioners, and applied researchers in the various domains of system analysis.

Goal

The goal of the LfSA workshop is to bring together scientists working on topics related to logics for system analysis for various system models and promote sharing and dissemination of ideas in their various application domains. In particular, we want to:

  • bring together experts in logics and experts in system analysis,
  • exchange concepts, experiences, and visions for logic-based description and analysis of systems,
  • facilitate technology transfer to different application domains,
  • provide a forum to exploit synergies among different application scenarios (e.g., different kinds of systems, different logic-based methods),
  • discuss consequences and synergies of the increasing convergence of systems that were previously considered unrelated (e.g., embedded systems and distributed systems, medical and robotic systems, digital circuits and analog circuits),
  • examine the application of academic results and methods to problems of industrial relevance.

    • Topics

    The scope of LfSA includes topics such as, theory, applications, and tools of:

  • Logics for safety-critical systems, including real-time systems, embedded systems, hybrid systems, distributed systems, stochastic systems, cyber-physical systems
  • Logic-based methods for the development of safety-critical systems, in- cluding requirements analysis, design, specification, and verification
  • Logic-based methods to study security aspects of systems or protocols
  • System representations in terms of logics, automata, modeling languages, state charts, Petri nets, dataflow models
  • Theories, decision procedures, and calculi for system analysis
  • Model checking, abstraction, and systematic testing for system analysis
  • Case studies for logical system analysis
  • Applications of system analysis to problems of industrial relevance, including automotive, aviation, railway, robotics, automation design, process control, mixed analogue/digital circuits in chip design

    • In particular, we invite contributions that bridge the gap between theory and practice or that combine features of multiple application domains.