Formal Methods && Tools Group

Current Research activity

Applications of formal methods in software engineering

  • Formalization of requirements as temporal logic formulae
  • Applications of Natural Language Processing techniques to the analysis of requirements documents
  • Development of tools for the automatic analysis of defects in Natural Language Requirements
  • Process mining and formal modelling of Business Processes

Formal Approaches to Safety-Critical Systems

  • Model driven development of Railway Control Systems
  • Formal Specification of Railway Interlocking Systems

Formal Approaches to Product Family Engineering

  • Logics for modeling behavioral variability
  • Development of behavioral models for product families

Advances in formal modeling and applications

  • Team Automata and Language Theory
  • Algorithmic network models of spacetime

Formal Modelling and Verification of Service-Oriented Systems

  • Development of new qualitative and quantitative temporal logics for specifying services and mobile computations properties
  • Development of new languages for modelling stochastic behaviour for services and mobile computations
  • Verification techniques for Abstract Service-Oriented Properties
  • Model-checking algorithms and tools

Formal Modelling and Verification of Collective Adaptive Systems

  • Development of qualitative and quantitative spatio-temporal logics for specifying properties in the context of population models
  • Development of quantitative process languages for specifying population models
  • Fluid-flow and Mean-Field semantics
  • Fluid-flow and Mean-Field based scalable model-checking algorithms
  • Application of CAS technology to smart city system design (e.g. bike-sharing, public transportation)

Past Research activity

  • Precise UML
    • Formal Semantics of UML Statechart Diagrams
    • Extensions of UML Statechart Diagrams (Stochastic time, Multicharts)
    • Testing theory and Formal Test Derivation from UML Statechart Diagrams
  • Specification Styles
    • Transposition of the concept of LOTOS constraint-oriented specification style to other languages, including Java and the original 'conotation'
  • Integration of process-algebraic and state-based and functional specification models
    • Extensions of Gurevich-Boerger Abstract State Machines for concurrent systems
    • Definition of Abstract State Processes
  • Formal Methods in Molecular Biology and Digital Physics

Formal Approaches to the modeling of Human-Computer Interaction

  • Modeling Continuous Interaction
  • Stochastic Time Modeling of Human Computer Interaction
  • HCI in Safety-Critical Systems
  • Novel devices