MLQA 2013

The fifth annual meeting of the MLQA working group will take place on Sunday 24 March 2013 as part of the European Joint Conferences on Theory And Practice of Software (ETAPS) in Rome, Italy. The details of the meeting will be posted on this page soon.

---

Invited speakers

• Martin Fränzle, University of Oldenburg
  To be announced
• Paolo Zuliani, Newcastle University
  Statistical Model Checking for Cyber-Physical Systems
• Flemming Nielson, Technical University of Denmark
  Guarding against Denial of Service Attacks

Abstracts of the invited talks are available here.

---

Registration

TBA

---

Preliminary Programme

TBA

---

Travel and Accommodation

TBA

---

Minutes

Minutes of MLQA 2013 will be available after the workshop.

---

Abstracts of Invited Talks

• Martin Fränzle, University of Oldenburg
  Title: To be announced
  Abstract: To be announced.
• Paolo Zuliani, Newcastle University
  Title: Statistical Model Checking for Cyber-Physical Systems
  Abstract: Statistical model checking is a simulation-based approach for verifying temporal logic properties of complex stochastic systems. Traditional model checking techniques work by searching efficiently the entire state space of the system. However, many interesting systems (e.g., cyber-physical systems) have exceedingly large, or even infinite, state spaces. This makes techniques based on exhaustive search unfeasible. Statistical model checking is instead based on sampling and system simulation, and thereby scales better with system size. We present a statistical model checking approach based on Bayesian statistics, and we apply it to cyber-physical systems coded as Stateflow/Simulink models. Next, we illustrate recent developments involving rare events and non-deterministic systems. We conclude by discussing the strength and weaknesses of the approach and possible directions for future research.
  
  
• Flemming Nielson, Technical University of Denmark
  Title: Guarding against Denial of Service Attacks
  Abstract: We outline an approach to the design of systems ensuring that the best possible operation is guaranteed even in the presence of denial of service attacks. As our vehicle of exposition we choose a process calculus allowing to time-out on expected inputs, to base subsequent actions on the extent to which expected inputs were successful and to suitably encrypt the messages exchanged. This is accompanied by an array of analysis techniques for determining the extent to which suitable caution has been exercised: a robustness analysis for ensuring that default data are available when actual data is missing, a safety and security analysis for additionally ensuring that flow of information does not violate integrity models like the Biba model, and a quantitative analysis for determining the probability distributions over the trustworthiness of the data upon which decisions are made.