Jose Meseguer

Formal Design of Cloud Computing Systems in Maude

Computer Science Department University of Illinois at Urbana-Champaign, USA

Abstract. Cloud computing systems are complex distributed systems whose design is challenging for two main reasons: (1) since they are distributed systems, a correct design is very hard to achieve by testing alone; and (2) cloud computing applications have high performance requirements such as low latency and high throughput; but this is hard to measure before implementation and hard to compare between different implementations. I will report on our experience on using formal specification in Maude and formal model checking analysis to quickly explore the design space of a cloud computing system to achieve a high quality design that: (1) has verified correctness guarantees; (2) has better performance properties than other design alternatives so explored; (3) can be achieved before any actual implementation; and (4) can be used for both rapid prototyping and for automatically code generation.

Biographical sketch. Jose Meseguer received his Ph.D. in Mathematics from the University of Zaragoza, Spain. He is Professor of Computer Science at the University of Illinois at Urbana-Champaign (UIUC). Prior to moving to UIUC he was a Principal Scientist as the Stanford Research Institute (SRI), after having held postdoctoral positions at the University of California at Berkeley and IBM Research. He was also an Initiator Member of Stanford University's Center for the Study of Language and Information (CSLI).

Meseguer has made fundamental contributions in the frontier between mathematical logic, executable formal specification and verification, declarative programming languages, programming methodology, programming language semantics, concurrency, and security. His work in all these areas, comprising over 375 publications, is very highly cited. His contributions to security include fundamental concepts such as nointerference, browser security verification, new algorithms and verification techniques to defend systems against Denial of Service (DoS) attacks, and new symbolic techniques to analyze cryptographic protocols modulo complex algebraic properties that have been embodied in the Maude-NPA Protocol Analyzer. He is the creator of rewriting logic, a very flexible computational logic to specify concurrent systems. The 2012 rewriting logic bibliography has over 1,000 publications. The Maude rewriting logic language is one of the most advanced and efficient executable formal specification languages worldwide. It supports a wide range of formal analyses, including symbolic simulation, search, model checking, and theorem proving. It is also an advanced declarative concurrent language with sophisticated object-oriented features and powerful module composition and reflective meta-programming capabilities. He, his collaborators, and other researchers have used Maude and its tool environment to build sophisticated systems and tools, and to specify and analyze many systems, including cryptographic protocols, network protocols, cloud computing systems, web browsers, cyber-physical systems, models of cell biology, executable formal semantics of programming and software modeling languages, formal analyzers for conventional code, theorem provers, and tools for interoperating different formal systems. He has given numerous invited lectures at international scientific meetings and has taught advanced courses on his research at leading American, British, German, Spanish, Italian, and Japanese universities and research centers. He has also served in numerous program committees of international scientific conferences and as editor of various scientific journals.

CALL FOR PAPERS

CALL FOR PAPERS

21st Brazilian Symposium On Formal Methods (SBMF)
Supported by the Brazilian Computer Society (SBC)
Salvador-BA, Brazil
26 to 30 of November 2018

IMPORTANT DATES

Paper Submission (EXTENDED) Deadline: **July 20th, 2018**
Paper Acceptance Notification: August 28th, 2018
Paper Camera-ready Version: September 11th, 2018

INTRODUCTION

SBMF 2018 is the twenty-first of a series of events devoted to the development, dissemination, and use of formal methods for the construction of high-quality computational systems. It is now a well-established event, with an international reputation.

In 2018, SBMF will take place in Salvador, the capital of the Bahia state, northeast of Brazil. It is the 3rd city by population in Brazil, with over 2.9 million inhabitants, and it is the second most popular destination in Brazil for tourists.

SCOPE AND TOPICS

• The aim of SBMF is to provide a venue for the presentation and discussion of high-quality work in formal methods. The topics include (not limited to):
• techniques and methodologies, such as method integration; software and hardware co-design; model-driven engineering; formal aspects of popular methodologies; formal design; development methodologies with formal foundations; software evolution based on formal methods;
• specification and modeling languages, such as well-founded specification and design languages; formal aspects of popular languages; logic and semantics for programming and specification languages; code generation; formal methods of programming paradigms (such as objects, aspects, and component), formal methods for real-time, hybrid, and safety-critical systems, formal models of service-oriented, cloud-based, and cyber-physical systems;
• theoretical foundations, such as domain theory; type systems and category theory; computational complexity of methods and models; computational models; term rewriting; models of concurrency, security and mobility;
• verification and validation, such as abstraction, modularization and refinement techniques; program and test synthesis; correctness by construction; model checking; theorem proving; static analysis; formal techniques for software testing; software certification; formal techniques for software inspection;
• Experience reports regarding teaching formal methods;
• applications, such as experience reports on the use of formal methods; industrial case studies; tool support.

PAPER SUBMISSION

Papers should present unpublished and original work that has a clear contribution to the state of the art on the theory and practice of formal methods. They should not be simultaneously submitted elsewhere.

Papers will be judged by at least three reviewers on the basis of originality, relevance, technical soundness and presentation quality, and should contain sound theoretical or practical results. Industry papers should emphasize practical application of formal methods or report on open challenges.

Contributions should be written in English and be prepared using Springer’s Lecture Notes in Computer Science (LNCS) format. Papers may not exceed 16 pages (including figures, references, and appendix). Accepted papers will be published, after the conference, in a volume of LNCS. Also, a special issue of Science of Computer Programming (Elsevier) is going to be published for the very best papers.

Every accepted paper MUST have at least one author registered in the symposium by the time the camera-ready copy is submitted; the registered author is also expected to attend the symposium and present the paper.

Papers can be submitted via the following link: https://easychair.org/conferences/?conf=sbmf2018

ABOUT SALVADOR

Salvador's importance dates back to Brazilian colonization, as it was established as the country's first capital (founded in 1549). Its center is a living museum of 17th- and 18th-century architecture and gold-laden churches. Aside from the many attractions within Salvador (Pelourinho, Modelo Public Market, Lacerda elevator, Church of Nosso Senhor do Bonfim), gorgeous coastline lies right outside the city – a suitable introduction to the tropical splendor of the state of Bahia.

Salvador presents a vibrant musical scene and popular Carnival celebrations, being considered one of the birthplaces of Brazilian culture.

Alexandre Mota

Alexandre Mota received his PhD degree in Computer Science from Universidade Federal de Pernambuco. The Brazilian Computer Society (SBC) awarded his PhD thesis. Since 2001 he is a professor of the Informatics Center (CIn) at Universidade Federal de Pernambuco. He holds a scholarship as Technological Productive Researcher from CNPq (the Brazilian National Research Agency), since 2012.

His research interests include the process algebra CSP, testing and model checking, theorem proving, formal modelling and refinement, dependability, and Experimental Software Engineering, based on tests and probabilistic simulations.

From 2005 to 2009 he has collaborated as a researcher in a research project between CIn and Motorola Mobility, focused on testing mobile phones (Stress and GUI-­‐based testing). From 2011 to 2014 he was a deputy (Brazilian side) of the COMPASS Project (Comprehensive Modelling for Advanced Systems of Systems), financed by the European Community FP7. And since 2006 he has been collaborating with Embraer, focusing on safety assessment and model-based testing. He is now coordinating as well as collaborating as a researcher in a new research project initiative between CIn and Motorola Mobility towards smartphone testing that started since 2015.

Title: The pragmatic dimension of Formal Methods: Tools Abstract: Formal methods are mathematically based languages, tools and techniques for the specification, development and verification of systems. To become practical, formal methods are supported by software tools: static analysers, model checkers, theorem provers, proof checkers, etc. Based on these tools and on the reuse principle of Software Engineering, during the years we have created several solutions that were applied from INPE (National Institute for Space Research) to Embraer. But the formal tools we have used to base our own work were developed as any software system, that is, ad hoc (and sometimes, semi-formally). In this talk we present these works and also some reasons formal tools are not developed formally and what we should do in the future to better convince others (and ourselves) to use formal methods to develop our own tools.

Jim Davies

Jim Davies is Professor of Software Engineering at the University of Oxford, and a group leader within the Oxford Big Data Institute. He is leading a national programme of infrastructure development - the NIHR Health Informatics Collaborative - aimed at improving the quality and availability of routinely-collected data for translational research. He was Chief Technology Officer of Genomics England Limited from 2013 to 2017. His research interests include model-driven engineering, process modelling, and health data science.

Title: Formal methods in health data science

Progress in the field of human health is increasingly reliant upon the acquisition, processing, and analysis of large volumes of complex, heterogeneous data. This represents a significant research challenge. The validity of our results, the correctness of our processing, and the safety of our applications all rely upon an adequate understanding of the data: its intended interpretation, and the context in which it is acquired. Interpretations may vary, context is infinite, and both may change over time.

Formal methods have an important role to play in addressing this challenge. In particular, set-theoretic notions of abstract data types and data refinement support the development of tools and theories for capturing our understanding of data and ensuring it is correctly reflected in any acquisition, processing, and analysis. In this talk, we will introduce a theory of real-world data semantics, and explain how it has been applied in the design and delivery of national programmes in health science.

Leo Freitas

Title:
There is no Royal Road: dependable and formal reasoning applied to medical-device development and certification.

Extended Abstract:
This talk is concerned with the adaptation and practical use of sound formal techniques to contribute to the risk analysis, notified body accreditation (i.e. CE-marking), and dependable development of life-critical medical devices.

The work involved a new methodology for the identification, adaptation, and application of stable and industry-standard formal techniques. It is tailored at aiding the reality of biomedical engineers, whom have no/little prior knowledge/training in formalism, in the gruelling medical certification process. It has been applied to three new medical devices:

1) a neonatal (baby < 5kg) dialysis machine for the UK national health service (NHS);

2) an optogenetic-based brain pacemaker research project primarily focusing on novel treatments for epilepsy (www.cando.ac.uk);

3) a preservation control system in transplants.

The work focuses on the formal analysis of the controller-component design and its software implementation on each of these devices. These controllers drive the medical activity (e.g. dialysis cycle, brain signals, organ preservation) and deals with error and alarm management, both critical to deliver treatment and to ensure adequate user experience (i.e. low alarm fatigue) in intensive care units.

Like with other embedded safety-critical systems, access to the ``real-world rig'' conditions is limited and difficult. On the other hand, medical certification requires a specific number of adequate usage within (real/ill) target patients. Testing is often difficult because the device is interacting with a ``physiological system'' (i.e. a human), and the cases where the device use may fail are rare. These and other factors make in-vivo testing very difficult indeed. Nevertheless, it is clear that developing a risk analysis is essential when dealing with life-critical medical systems.

Medical device standards require measures to be taken against risks associated with use of devices, and to keep such risks as low as reasonably practicable. These ``(un)known unknown'' conditions present an interesting (and novel) challenge to the application of formal techniques. Conventionally, risk analyses submitted to the regulator use clinical trial data as evidence that requirements have been satisfied and the device is safe for patient use. This is an onerous task requiring substantial amounts of test data, often under expensive clinical settings under special medical-trial permissions.

Our risk analysis was designed to satisfy regulatory requirements by presenting evidence for the technical file compiled as required by regulatory authorities (e.g. UK MHRA, US FDA, etc.). Guidelines typically assess the hazards associated with a medical device. These hazards include possible hardware and software failures. A key aim is to push regulations towards allowing evidence provided through formal reasoning to be accepted in lieu of clinical-trial data. This is inline with other safety-critical industries like the use of formal methods in DO-178C for avionics software compliance.

The risk analysis we developed use a combination of model based design, model checking, and theorem proving techniques for the engineering designs; and source-code analysis for freedom of certain run-time errors, as well as functional (total/partial) correctness including the use of pointers and shared memory in low-level C/C++ programs. To date, the work has provided the following encouraging evidence/results:

1) The verification of risk control measures relating to the state-machine design and low-level C software components in the dialyser. The productive dialogue between the developers of the device, who had no prior experience or knowledge of formal methods, and our formal analysis techniques, provided a basis for a rationale on the effectiveness of the evidence presented for certification, which has now been granted. It also identified, and mitigated, a rare (but life-threatening) problem within the system. This device has been (UK) certified and its IP commercialised.

2) Like with the dialyser's software, we provided total functional correctness of key device driver and low-level firmware C code for the special-purpose CMOS-chip being used in animal trials. After identifying interesting issues and hidden assumptions about the current version of the CMOS-chip drivers, we are now participating in the design of the new chip's command-set, as well as its low-level C device-drivers, to be used in human trials in a couple of years time. The work has now featured in the technical file being prepared for the upcoming device certification.
3) Different from the previous two examples, where our interventions occurred at the end and in middle of development, we have participated from the beginning in the preservation control system example. Together with biomedical engineer colleagues, we have applied these formal techniques to the design of the control systems and its complex conditions. Results to date include pending patents on algorithms and initial formal control-system designs. This device has commercial interest and will be certified.

MOHAMMAD MOUSAVI

Mohammad got his Ph.D. in Computer Science from Eindhoven University of Technology, The Netherlands in 2005. Since then he held positions at Reykjavik University (postdoctoral researcher), Eindhoven University of Technology (assistant and associate professor), Delft University of Technology (guest faculty member), Halmstad University (professor of Computer Systems Engineering), and Chalmers / University of Gothenburg (guest professor of Software Engineering). Mohammad's main research area is in model-based testing, particularly applied to software product lines and cyber-physical systems.

Title: Conformance Testing as a Tool for Designing Connected Vehicle Functions

Abstract: Connected and Autonomosu Vehicles (CAV) are taking a central position in the landscape of intelligent mobility and their rigorous verification and validation is one of the main challenges in their public deployment and social acceptance. Conformance testing is a rigorous verification technique that has been widely tried in various critical applications. In this talk, we examin the adaptations and extensions of conformance testing techniques that make them suitable for application in the CAV domain. We present how the extended techniques can be used in the design of connected vehicle functions and verify various design decisions.

Accepted Papers

Source Code Analysis with a Temporal Extension of First-Order Logic

David Come, Julien Brunel and David Doose

A Type-Directed Algorithm to Generate Well-Typed Featherweight Java Programs

Samuel Feitosa, Rodrigo Geraldo Ribeiro and Andre Rauber Du Bois

Programming Language Foundations in Agda

Philip Wadler

Formal Verification of n-bit ALU using Theorem Proving

Sumayya Shiraz and Osman Hasan

The Scallina Grammar - Towards a Scala Extraction for Coq

Youssef El Bakouny and Dany Mezher.

VDM at large: Modelling the EMV(R) 2nd Generation Kernel

Leo Freitas

Constraint Reusing and k-induction for Three-Valued Bounded Model Checking

Nils Timm, Stefan Gruner and Matthias Harvey

TeSSLa: Temporal Stream-based Specification Language

Lukas Convent, Sebastian Hungerecker, Martin Leucker, Torben Scheffel, Malte Schmitz and Daniel Thoma

Automatic Test Case Generation for Concurrent Features from Natural Language Descriptions

Rafaela Almeida, Sidney Nogueira and Augusto Sampaio

A Methodology for Protocol Verification applied to EMV

Leo Freitas, Paolo Modesti and Martin Emms

Analysing RoboChart with Probabilities

Madiel Conserva Filho, Rafael Marinho, Alexandre Mota and Jim Woodcock

Timed Scenarios: Consistency, Equivalence and Optimization

Neda Saeedloei and Feliks Kluzniak

Safe and Constructive Design with UML Components

Flávia Falcão, Lucas Lima and Augusto Sampaio

Formal modelling of environment restrictions from natural-language requirements

Tainã Santos, Gustavo Carvalho and Augusto Sampaio

History

In 2018, SBMF reaches the 21st edition of a well established meeting for both the Brazilian and the international researchers on Formal Methods. SBMF started as the Workshop on Formal Methods (WMF) in 1998 and became the Brazilian Symposium on Formal Methods (SBMF) in 2004.

III ETMF 2018 - 26 E 27 DE NOVEMBRO DE 2018 - SALVADOR, BA, BRASIL

EVENTO SATÉLITE DO SIMPÓSIO BRASILEIRO DE MÉTODOS FORMAIS (SBMF)

A Terceira Escola de Informática Teórica e Métodos Formais (ETMF 2018) é uma promoção conjunta da Universidade Federal da Bahia (UFBA) e Universidade Federal de Pernambuco (UFPE). A escola é um evento satélite do Simpósio Brasileiro de Métodos formais e visa congregar estudantes e pesquisadores para divulgar e promover aspectos teóricos da computação, particularmente:

qualificar a formação de estudantes e profissionais nas áreas que compõem a informática teórica;

prover um fórum onde possam ser apresentados os trabalhos em andamento nessas áreas, recebendo retorno de outros pesquisadores.

Programa

Segunda-feira 26/11
08:30 - 09:00 Credenciamento
09:00 - 10:30 Minicurso 1 (Parte 1) - Thierry Lecomte
10:30 - 11:00 Intervalo
11:00 - 12:30 Minicurso 2 (Parte 1) - Gustavo Carvalho
14:00 - 15:30 Minicurso 1 (Parte 2) - Thierry Lecomte
15:30 - 16:00 Intervalo
16:00 - 17:30 Minicurso 2 (Parte 2) - Gustavo Carvalho

Terça-feira 27/11
08:30 - 09:00 Credenciamento
09:00 - 10:30 Minicurso 3 (Parte 1) - Mohammad Reza Mousavi
10:30 - 11:00 Intervalo
11:00 - 12:30 Minicurso 4 (Parte 1) - Marlo Souza
14:00 - 15:30 Minicurso 3 (Parte 2) - Mohammad Reza Mousavi
15:30 - 16:00 Intervalo
16:00 - 17:30 Minicurso 4 (Parte 2) - Marlo Souza

Minicursos

MINICURSO 01: O sistema de provas Atelier B e suas melhorias
Palestrante: Thierry Lecomte (ClearSy Systems Engineering)
Resumo: Um desenvolvimento formal exige que diferentes aspectos sejam verificados usando provas matemáticas. O Atelier B produz automaticamente várias obrigações de prova (POs). Para ajudar o usuário a provar estas obrigações, o Atelier B incluiu um provador de teoremas desde o seu início. Esse provador de teorema "histórico" é um mecanismo de inferência e um banco de dados de regras (extensível). O sistema foi certificado no domínio ferroviário por revisão de especialistas. A arquitetura do provador de teoremas é construída de tal forma que pode ser usada interativa ou automaticamente em diferentes níveis. Durante este tutorial “mão na massa", serão apresentados o sistema de provas Atelier B, baseado neste provador de teoremas, bem como algumas capacidades de interação, além de experimentação com vários exemplos significativos. Uma atenção especial será dada aos mecanismos de automação e extensão que permitem facilitar o trabalho de prova e reduzir o tempo para concluir a demonstração de obrigações de prova.

 

MINICURSO 02: Reasoning with the Coq proof assistant
Palestrante: Gustavo Carvalho, CIn-UFPE, Brazil
Resumo: Coq é um provador de teoremas interativo para auxiliar no desenvolvimento de provas verificadas por máquinas. Entre suas muitas aplicações, ele pode ser usado para certificar propriedades de linguagens de programação e para provar a correção de algoritmos. Neste breve curso, abordaremos os conceitos básicos do Coq: definições indutivas, programação funcional com o Coq e a linguagem de táticas.

 

MINICURSO 03: Model-Based Testing: From Theory to Practice and Back 
Palestrante: Mohammad Reza Mousavi,  University of Leicester, UK 

Resumo: Teste e depuração respondem por mais da metade dos custos de desenvolvimento de software e estão se tornando sérios gargalos no processo de desenvolvimento de software. O problema é intensificado para sistemas embarcados e ciber-físicos devido à complexa interação entre software, hardware e o mundo físico. No estado atual da prática, os sistemas embarcados e ciber-físicos são frequentemente testados muito tarde no processo, ou testados de menos, de maneira ad-hoc e não-estruturada. Uma solução promissora para estes problemas está nos processos automatizados de Testes Baseados em Modelos (MBT), que fornecem uma abordagem estruturada para testes de modelos comportamentais de alto nível. Neste tutorial, começaremos com os princípios básicos de testes de software e sistema. Em seguida, apresentaremos os fundamentos de testes baseados em modelos e uma visão geral dos modelos e ferramentas atualmente disponíveis. A parte avançada do tutorial se concentrará em duas áreas de pesquisa em evolução: a primeira diz respeito ao teste de linhas de produtos de software, que envolve lidar com a grande variabilidade e formas eficazes de tratá-las. A segunda área envolve testes de sistemas ciberfísicos, onde não apenas o comportamento discreto do sistema de computador precisa ser testado, mas também sua interação com o comportamento contínuo dos componentes físicos precisa ser levada em conta.

MINICURSO 04: Completeza e Complexidade de sistemas dedutivos para Lógicas Modais, Multimodais e de Descrição
Palestrante: Marlo Souza, UFBA, Brazil
Resumo: Lógicas Modais são uma família de lógicas não verifuncionais que possuem um operador de qualificação de informação, como 'é necessário que', 'é desejável que', ou 'sabe-se que'. Tais lógicas vêm recebendo crescente atenção de áreas como a Filosofia, a Ciência da Computação e a Inteligência Artificial dada a flexibilidade, expressividade e interessantes propriedades computacionais que possuem, sendo aplicadas como linguagens que fundamentam teorias e sistemas de Especificação e Verificação Formal, Representação do Conhecimento e Sistemas Cognitivos. Enquanto para algumas lógicas modais, sistemas de dedutivos com complexidade computacional conhecida são facilmente obtidos através de resultados canônicos da teoria da correspondência, tais resultados já não fornecem ferramentas necessárias para contemplar a diversidade de lógicas modais propostas na literatura atual. Particularmente, tais resultados não podem ser aplicados para analisar lógicas  modais com aplicações interessantes na Ciência da Computação e Inteligência Artificial, como lógicas de preferências bem-fundadas usadas em raciocínio não-monotônico, ou lógicas de descrição  usadas em representação de conhecimento. Prover, então, sistemas dedutivos completos para tais lógicas e analisar sua complexidade computacional se torna um problema não trivial. Este tutorial almeja explorar resultados clássicos da teoria de correspondência para lógicas modais proposicionais, como modelos canônicos, exemplos de axiomas não canônicos e combinação de lógicas modais  para prover resultados de completeza e complexidade de lógicas modais, multimodais e de descrição bem conhecidas.