Search for Articles:
Title / Keyword
Author / Affiliation / Email
Journal
Article Type
 
 
Advanced Search
 
Section
Special Issue
Volume
Issue
Number
Page
 
5.8
3.1
Journals
Information
Special Issues
Formal Methods for Verification and Control of Cyberphysical Systems
share announcement

Formal Methods for Verification and Control of Cyberphysical Systems

A special issue of Information (ISSN 2078-2489). This special issue belongs to the section "Information Systems".

Deadline for manuscript submissions: closed (15 May 2021) | Viewed by 5372

Special Issue Editor

Dr. Federico Mari

E-Mail Website
Guest Editor
Department of Movement, Human and Health Sciences, University of Rome Foro Italico, 00135 Rome, Italy
Interests: model checking; control software generation; cyberphysical systems; hybrid systems

Special Issue Information

Dear Colleagues,

We invite you to submit to the Special Issue “Formal Methods for Verification and Control of Cyberphysical Systems” which may involve novel methods, implementation of software tools, or concrete case studies.

Cyberphysical systems (CPSs) have become increasingly important and widespread in safety- and mission-critical contexts such as, for example, concerning smart grids, avionics, automotives, and Industry 4.0. The verification and control of CPSs, needed in such delicate conditions, are unfortunately computationally difficult problems.

Despite these challenges, formal methods that have been successfully applied in recent decades have contributed tremendously to developing the field. Nonetheless, further efforts are still needed to improve the applicability and efficiency of formal methods for CPS case studies as well as of widespread formal methods for use in the context of Industry 4.0.

The scope of this Special Issue is generally on formal methods as applied to the verification and control of CPSs. In particular, the scope includes but is not limited to the following topics:

  • Automatic verification of CPSs (e.g., model checking, simulation-based techniques, etc.)
  • Automatic control of CPSs (e.g., optimal, distributed and networked, planning, etc.)
  • Symbolic methods for verification and control of CPSs (e.g., satisfiability modulo theories, etc.)
  • Statistical methods for verification and control of CPSs (e.g., statistical model checking, techniques based on machine learning, data analytics, etc.)
  • Implementation in software tools of verification and control methods of CPS
  • Presentation of case studies on verification and control of CPS (e.g., smart grids, avionics, biology, etc.)

Dr. Federico Mari
Guest Editor

Manuscript Submission Information

Manuscripts should be submitted online at www.mdpi.com by registering and logging in to this website. Once you are registered, click here to go to the submission form. Manuscripts can be submitted until the deadline. All submissions that pass pre-check are peer-reviewed. Accepted papers will be published continuously in the journal (as soon as accepted) and will be listed together on the special issue website. Research articles, review articles as well as short communications are invited. For planned papers, a title and short abstract (about 100 words) can be sent to the Editorial Office for announcement on this website.

Submitted manuscripts should not have been published previously, nor be under consideration for publication elsewhere (except conference proceedings papers). All manuscripts are thoroughly refereed through a single-blind peer-review process. A guide for authors and other relevant information for submission of manuscripts is available on the Instructions for Authors page. Information is an international peer-reviewed open access monthly journal published by MDPI.

Please visit the Instructions for Authors page before submitting a manuscript. The Article Processing Charge (APC) for publication in this open access journal is 1600 CHF (Swiss Francs). Submitted papers should be well formatted and use good English. Authors may use MDPI's English editing service prior to publication or during author revisions.

Keywords

  • cyberphysical systems
  • verification
  • control
  • formal methods
  • model checking
  • satisfiability modulo theories

Published Papers (2 papers)

Download All Papers
Order results
Result details
Show export options expand_more Show export options expand_less
Select all
Export citation of selected articles as:

Research

Jump to: Review

19 pages, 854 KiB  
Article
Visualisation of Control Software for Cyber-Physical Systems
by Igor Melatti, Federico Mari, Ivano Salvo and Enrico Tronci
Information 2021, 12(5), 178; https://0-doi-org.brum.beds.ac.uk/10.3390/info12050178 - 21 Apr 2021
Viewed by 1760
Abstract
Cyber-physical systems are typically composed of a physical system (plant) controlled by a software (controller). Such a controller, given a plant state s and a plant action u, returns 1 iff taking action u in state s leads [...] Read more.
Cyber-physical systems are typically composed of a physical system (plant) controlled by a software (controller). Such a controller, given a plant state s and a plant action u, returns 1 iff taking action u in state s leads to the physical system goal or at least one step closer to it. Since a controller K is typically stored in compressed form, it is difficult for a human designer to actually understand how “good” K is. Namely, natural questions such as “does K cover a wide enough portion of the system state space?”, “does K cover the most important portion of the system state space?” or “which actions are enabled by K in a given portion of the system space?” are hard to answer by directly looking at K. This paper provides a methodology to automatically generate a picture of K as a 2D diagram, starting from a canonical representation for K and relying on available open source graphing tools (e.g., Gnuplot). Such picture allows a software designer to answer to the questions listed above, thus achieving a better qualitative understanding of the controller at hand. Full article
(This article belongs to the Special Issue Formal Methods for Verification and Control of Cyberphysical Systems)
►▼ Show Figures

Figure 1

Review

Jump to: Research

24 pages, 450 KiB  
Review
Monte Carlo Based Statistical Model Checking of Cyber-Physical Systems: A Review
by Angela Pappagallo, Annalisa Massini and Enrico Tronci
Information 2020, 11(12), 588; https://0-doi-org.brum.beds.ac.uk/10.3390/info11120588 - 21 Dec 2020
Cited by 12 | Viewed by 2572
Abstract
The ever-increasing deployment of autonomous Cyber-Physical Systems (CPSs) (e.g., autonomous cars, UAV) exacerbates the need for efficient formal verification methods. In this setting, the main obstacle to overcome is the huge number of scenarios to be evaluated. Statistical Model Checking (SMC) is a [...] Read more.
The ever-increasing deployment of autonomous Cyber-Physical Systems (CPSs) (e.g., autonomous cars, UAV) exacerbates the need for efficient formal verification methods. In this setting, the main obstacle to overcome is the huge number of scenarios to be evaluated. Statistical Model Checking (SMC) is a simulation-based approach that holds the promise to overcome such an obstacle by using statistical methods in order to sample the set of scenarios. Many SMC tools exist, and they have been reviewed in several works. In this paper, we will overview Monte Carlo-based SMC tools in order to provide selection criteria based on Key Performance Indicators (KPIs) for the verification activity (e.g., minimize verification time or cost) as well as on the environment features, the kind of system model, the language used to define the requirements to be verified, the statistical inference approach used, and the algorithm implementing it. Furthermore, we will identify open research challenges in the field of (SMC) tools. Full article
(This article belongs to the Special Issue Formal Methods for Verification and Control of Cyberphysical Systems)
►▼ Show Figures

Figure 1

Show export options expand_more Show export options expand_less
Select all
Export citation of selected articles as:
 
Displaying articles 1-2
Back to TopTop