ICTAC Conference | ICTAC 2021 | News | Important Dates | Overview and Scope | Call for Papers | Registration | Programme | Keynote Speakers | Committees | ICTAC School 2021
RoboStar group, Department of Computer Science, University of York, England, UK
Abstract:
Use of simulation to support the design of software for robotic systems is pervasive.
Typically, roboticists draw a state machine using an informal notation
(not precise or machine checkable) to convey a design and guide the development of a simulation.
This involves writing code for a specific simulator (using C, C++, or some proprietary language and API).
Reactive robotics simulators do not normally generate code for deployment. Instead, simulation code
is often reused after changes.
So, there is potential loss of properties observed via simulation: because of the possibility of
changes introducing errors, and because of the reality gap. The RoboStar technology supports a model-based,
rather than (simulation) code, approach to development.
Models are written using domain-specific notations in line with those accepted by roboticists.
In this course, we will focus on modelling and verification using RoboChart, our design notation, and its tool.
In RoboChart, software controllers are described by timed state machines.
The semantics is defined using a process algebra, namely, tock-CSP, which we use for verification.
Computational Foundry / Ffowndri Gyfrifiadol, Swansea University, Wales, UK
Abstract:
The first part of this lecture will give a lightening introdction to the use of formal methods in human–computer interaction.
This will include and overview of the kinds of models, and typical domains where techniques are currently applied.
It will then outline some of the potential future directions for the field based on the “Trends and Gaps” chapter of
“The Handbook of Formal Methods in Human-Computer Interaction”.
In the second part we will focus on a specific area, the formal specification and analysis of systems that have both physical and
digital aspects.
This will include using physigrams, a extension of finite state networks for describing interactions with physical devices such as
hand-held controllers.
We will also look at the ways formal analysis contributed to the design of an internet-enabled ‘cafe open’ sign – IoT in action!
School of Computer Science, University of St. Andrews, Scotland, UK
Abstract:
Formal methods have shown benefits across many domains, and are more commonly used for ensuring the correctness of critical systems.
This course shows how logic-based formalisms and automated tools can help to address a variety of problems that arise in the
healthcare domain.
One such example includes how to improve and personalise treatments for patients with multiple chronic conditions (aka multimorbidity)
and address patient safety concerns inherent in polypharmacy (e.g., the prescribing of 5 or more medications).
The combination of efficient and formal verification techniques, such as constraint solvers and theorem provers,
can be explored in this context to identify situations that arise and should be avoided when applying medical recommendations
for different chronic conditions simultaneously.
For example, drugs prescribed for different diseases may cause adverse reactions, health recommendations may contradict each other,
and/or undesired medication side effects may arise.
Instead, we would like to offer personalised treatments and find the preferred treatment for a patient in accordance to given
criteria (e.g. drug efficacy, prevalent disease, patient allergies, preferences, etc.).
In addition, this course will discuss how challenges arising in medicine can provide inspiration for further research on the
foundations of formal verification.
Department of Informatics, University of Oslo, Norway
Abstract:
Rewriting logic is a powerful and general, yet simple and intuitive,
logic for specifying dynamic systems, and is particularly suitable to
specify distributed computer systems in an object-oriented style.
Maude is a programming/modeling language and high-performance analysis
tool for rewriting logic. Data types are defined by equational
specifications (which operationally can be seen as rich term
rewrite systems), while dynamic behaviors are specified by
(possibly conditional) rewrite rules. Maude models can then be
subjected to: (a) simulation by rewriting; (b) reachability analysis
by search; (c) various forms of temporal logic model checking; (d)
symbolic analysis; and (e) various forms of theorem proving using
associated tools.
Maude has been successfully applied to a wide range of sophisticated
systems, including: transport protocols, cloud-based distributed
transaction systems, biological systems, human cognition, programming
and modeling language semantics and analysis, cyber-physical systems,
and so on.
This tutorial gives an introduction to specification and analysis in Maude.
It also briefly touches upon some applications of Maude, and
extensions to real-time and probabilistic systems.
Course Materials: Part 1, Part 2, Part 3.
RWTH Aachen University & Fraunhofer-Institut für Angewandte Informationstechnik (FIT), Germany
Abstract:
Process mining is the missing link between model-based process analysis and data-oriented analysis techniques.
Through concrete data sets and easy-to-use software, the course provides concepts and tools that can be applied directly
to analyze and improve processes in a variety of domains. The course explains the key analysis techniques in process mining.
Participants will learn about process discovery techniques.
These can be used to automatically learn process models from raw event data. Various other process analysis techniques
that use event data will be presented, including conformance checking.
Moreover, the course will provide access to easy-to-use software, real-life data sets, and practical skills to directly
apply the theory in a variety of application domains.
In recent years, we could witness a spectacular uptake in process mining. There used to be a gap between process science
(i.e., tools and techniques to improve operational processes) and data science (i.e., tools and techniques to extract value from data).
Mainstream machine learning and data mining techniques do not consider operational processes.
Business Process Management (BPM) and Operations Research (OR) tend to start from models rather than data.
Process mining bridges this gap.
Currently, there are over 35 commercial process mining vendors (ABBYY Timeline, ARIS Process Mining, BusinessOptix,
Celonis Process Mining, Disco/Fluxicon, Everflow, Lana, Mavim, MPM, Minit, PAFnow, QPR, etc.) and process mining is applied
in most of the larger organizations.
Example application domains include: finance (Rabobank, Hypovereinsbank, etc.), telecom (Deutsche Telekom, Vodafone, etc.),
logistics (Vanderlande, etc.), production (BMW, Siemens, Fiat, Bosch, etc.), food (Edeka, etc.), fashion (Zalando, etc.),
energy (E-on, etc.), transport (Uber, DB, Lufthansa, etc.), healthcare (AstraZenica, Medtronic, etc.),
consulting (Deloitte, EY, KPMG, etc.), and IT systems (Dell, IBM, ServiceNow, etc.).
The course will be at an introductory level. Participants should have a basic understanding of process and data modeling without
knowing a specific notation or language.
Participants are encouraged to download the provided process mining software and data sets.
The demo sessions will provide smaller examples and show the application of both open-source and commercial software to the data sets
provided.
Oracle Labs, Australia
Abstract:
In this presentation I will present a high level overview of various projects related to detecting security vulnerabilities.
These include static analyses, server-side dynamic analysis, client-side dynamic analysis, and malware analysis.
I will also outline the challenges that we overcame to ensure our research was deployed in practice.
I will conclude with some of the remaining challenges especially in the context of DevSecOps.
Course Materials (restricted to Nazarbayev University account holders)
Department of Computer Science, School of Engineering and Digital Sciences, Nazarbayev University, Kazakhstan
Abstract:
While formal methods provide powerful means by which designers can show that their systems meet specific requirements,
industry has been slow to incorporate them due to the perceived high cost of adoption.
In this talk, I will present my experiences working for a small business which developed and promoted formal methods tools
for use by public and government agencies, where the users were not necessarily specialists.
Specifically, I will discuss our use of a general-purpose design language, our development of intuitive graphics-based tools
to make the system design task easier, and how we applied automated model checking to the resulting system models.
I will also discuss our interaction with and feedback from clients regarding these tools.
Department of Computer Science, School of Engineering and Digital Sciences, Nazarbayev University, Kazakhstan
Abstract:
Because of their purely mathematical nature and high complexity, formal methods are often perceived in industrial contexts
as difficult to understand and detached from reality
In fact, many aspects of reality are intuitively understood and informally described using conceptual rather than formal models.
This is especially true in human-computer interaction, since, on the one hand, the human components of the overall system cannot be fully
characterised in mathematical terms, and, on the other hand, analyst may come from very different backgrounds, including social sciences,
and are unlikely to be expert in formal methods.
The first part of this short course introduces an intuitive notation to describe human reasoning and behaviour and shows how to use it
informally to analyse human behaviour and human-computer interaction.
The second part considers conceptual models of memory processes and human behaviour from cognitive psychology in order to provide
alternative formal semantics to the intuitive notation.
This allows us to reconcile our intuitive notation with some formal methods presented in previous courses of the school
in order to allow analysts who are not expert in formal methods to formally verify human-computer interactions.
Finally, the last part of the course, explores possible research developments in using formal methods to validate interactive
systems in the context of their real world usage.
12:45-13:00 - OPENING
13:00-17:00 -
Software Engineering for Robotics: RoboStar technology
Ana Cavalcanti,
James Baxter,
Pedro De Oliveira Salazar Ribeiro,
Alvaro Miyazawa
(University of York, UK)
17:00-18:00 - BREAK
18:00-20:00 -
Modelling interactions: digital and physical
Alan Dix
(Swansea University, UK)
15:00-16:00 -
A Tutorial to Maude (Part 1)
Peter Csaba Ölveczky
(University of Oslo, Norway)
16:00-17:00 -
Applying Formal Methods in Healthcare (Part 1)
Juliana Küster Filipe Bowles
(University of St. Andrews, UK)
17:00-19:00 - BREAK
19:00-20:00 -
Process Mining (Part 1: Introduction)
Wil van der Aalst
(RWTH Aachen University, Germany)
14:00-16:00 -
A Tutorial to Maude (Part 2)
Peter Csaba Ölveczky
(University of Oslo, Norway)
16:00-17:00 -
Applying Formal Methods in Healthcare (Part 2)
Juliana Küster Filipe Bowles
(University of St. Andrews, UK)
17:00-18:00 - BREAK
18:00-19:00 -
Process Mining (Part 2: Example algorithms)
Wil van der Aalst
(RWTH Aachen University, Germany)
19:00-20:00 -
Process Mining (Part 3: Applications)
Wil van der Aalst
(RWTH Aachen University, Germany)
14:00-15:00 -
Research and Industry (Security Research at Oracle Labs, Australia: Program Analysis Meets Security)
Padmanabhan Krishnan
(Oracle Labs, Australia)
15:00-16:00 -
Research and Industry (Formal Methods Adoption in Industry: An Experience Report)
Ben Tyler
(Nazarbayev University, Kazakhstan)
15:00-17:00 -
A Tutorial to Maude (Part 3)
Peter Csaba Ölveczky
(University of Oslo, Norway)
17:00-18:00 - BREAK
18:00-20:00 -
Analyzing interactions: informally and formally
Antonio Cerone
(Nazarbayev University, Kazakhstan)
7:45-8:00 - OPENING
8:00-12:00 -
Software Engineering for Robotics: RoboStar technology
Ana Cavalcanti,
James Baxter,
Pedro De Oliveira Salazar Ribeiro,
Alvaro Miyazawa
(University of York, UK)
12:00-13:00 - BREAK
13:00-15:00 -
Modelling interactions: digital and physical
Alan Dix
(Swansea University, UK)
10:00-11:00 -
A Tutorial to Maude (Part 1)
Peter Csaba Ölveczky
(University of Oslo, Norway)
11:00-12:00 -
Applying Formal Methods in Healthcare (Part 1)
Juliana Küster Filipe Bowles
(University of St. Andrews, UK)
12:00-14:00 - BREAK
14:00-15:00 -
Process Mining (Part 1: Introduction)
Wil van der Aalst
(RWTH Aachen University, Germany)
9:00-11:00 -
A Tutorial to Maude (Part 2)
Peter Csaba Ölveczky
(University of Oslo, Norway)
11:00-12:00 -
Applying Formal Methods in Healthcare (Part 2)
Juliana Küster Filipe Bowles
(University of St. Andrews, UK)
12:00-13:00 - BREAK
13:00-14:00 -
Process Mining (Part 2: Example algorithms)
Wil van der Aalst
(RWTH Aachen University, Germany)
14:00-15:00 -
Process Mining (Part 3: Applications)
Wil van der Aalst
(RWTH Aachen University, Germany)
9:00-10:00 -
Research and Industry (Security Research at Oracle Labs, Australia: Program Analysis Meets Security)
Padmanabhan Krishnan
(Oracle Labs, Australia)
10:00-11:00 -
Research and Industry (Formal Methods Adoption in Industry: An Experience Report)
Ben Tyler
(Nazarbayev University, Kazakhstan)
10:00-12:00 -
A Tutorial to Maude (Part 3)
Peter Csaba Ölveczky
(University of Oslo, Norway)
12:00-13:00 - BREAK
13:00-15:00 -
Analyzing interactions: informally and formally
Antonio Cerone
(Nazarbayev University, Kazakhstan)
8:45-9:00 - OPENING
9:00-13:00 -
Software Engineering for Robotics: RoboStar technology
Ana Cavalcanti,
James Baxter,
Pedro De Oliveira Salazar Ribeiro,
Alvaro Miyazawa
(University of York, UK)
13:00-14:00 - BREAK
14:00-16:00 -
Modelling interactions: digital and physical
Alan Dix
(Swansea University, UK)
11:00-12:00 -
A Tutorial to Maude (Part 1)
Peter Csaba Ölveczky
(University of Oslo, Norway)
12:00-13:00 -
Applying Formal Methods in Healthcare (Part 1)
Juliana Küster Filipe Bowles
(University of St. Andrews, UK)
13:00-15:00 - BREAK
15:00-16:00 -
Process Mining (Part 1: Introduction)
Wil van der Aalst
(RWTH Aachen University, Germany)
10:00-12:00 -
A Tutorial to Maude (Part 2)
Peter Csaba Ölveczky
(University of Oslo, Norway)
12:00-13:00 -
Applying Formal Methods in Healthcare (Part 2)
Juliana Küster Filipe Bowles
(University of St. Andrews, UK)
13:00-14:00 - BREAK
14:00-15:00 -
Process Mining (Part 2: Example algorithms)
Wil van der Aalst
(RWTH Aachen University, Germany)
15:00-16:00 -
Process Mining (Part 3: Applications)
Wil van der Aalst
(RWTH Aachen University, Germany)
10:00-11:00 -
Research and Industry (Security Research at Oracle Labs, Australia: Program Analysis Meets Security)
Padmanabhan Krishnan
(Oracle Labs, Australia)
11:00-12:00 -
Research and Industry (Formal Methods Adoption in Industry: An Experience Report)
Ben Tyler
(Nazarbayev University, Kazakhstan)
11:00-13:00 -
A Tutorial to Maude (Part 3)
Peter Csaba Ölveczky
(University of Oslo, Norway)
13:00-14:00 - BREAK
14:00-16:00 -
Analyzing interactions: informally and formally
Antonio Cerone
(Nazarbayev University, Kazakhstan)
16:45-17:00 - OPENING
17:00-21:00 -
Software Engineering for Robotics: RoboStar technology
Ana Cavalcanti,
James Baxter,
Pedro De Oliveira Salazar Ribeiro,
Alvaro Miyazawa
(University of York, UK)
21:00-22:00 - BREAK
22:00-24:00 -
Modelling interactions: digital and physical
Alan Dix
(Swansea University, UK)
19:00-20:00 -
A Tutorial to Maude (Part 1)
Peter Csaba Ölveczky
(University of Oslo, Norway)
20:00-21:00 -
Applying Formal Methods in Healthcare (Part 1)
Juliana Küster Filipe Bowles
(University of St. Andrews, UK)
21:00-23:00 - BREAK
23:00-24:00 -
Process Mining (Part 1: Introduction)
Wil van der Aalst
(RWTH Aachen University, Germany)
18:00-20:00 -
A Tutorial to Maude (Part 2)
Peter Csaba Ölveczky
(University of Oslo, Norway)
20:00-21:00 -
Applying Formal Methods in Healthcare (Part 2)
Juliana Küster Filipe Bowles
(University of St. Andrews, UK)
21:00-22:00 - BREAK
22:00-23:00 -
Process Mining (Part 2: Example algorithms)
Wil van der Aalst
(RWTH Aachen University, Germany)
23:00-24:00 -
Process Mining (Part 3: Applications)
Wil van der Aalst
(RWTH Aachen University, Germany)
18:00-19:00 -
Research and Industry (Security Research at Oracle Labs, Australia: Program Analysis Meets Security)
Padmanabhan Krishnan
(Oracle Labs, Australia)
19:00-20:00 -
Research and Industry (Formal Methods Adoption in Industry: An Experience Report)
Ben Tyler
(Nazarbayev University, Kazakhstan)
19:00-21:00 -
A Tutorial to Maude (Part 3)
Peter Csaba Ölveczky
(University of Oslo, Norway)
21:00-22:00 - BREAK
22:00-24:00 -
Analyzing interactions: informally and formally
Antonio Cerone
(Nazarbayev University, Kazakhstan)
