FVPS 2019

classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

FVPS 2019

gepr
Arg!  I wish I could go to this.  If any of you do, please send along some notes.

2nd Workshop on Formal Verification of Physical Systems (FVPS 2019)
https://www.cicm-conference.org/2019/cicm.php?event=fvps&menu=general

> Theme
>
> One of the main issues behind many failing systems is the ad-hoc verification approach that involves a variety of formalism and techniques for the modeling and analysis of various components of the present-age (cyber)-physical systems. For example, control and communication protocols are usually modeled using automata theory, and thus analyzed using model checking techniques, while the modeling of physical aspects often require multivariate calculus foundations, which are in turn analyzed using paper-and-pencil based analytical proofs, simulation or theorem proving. The fundamental differences between these modeling and analysis techniques limit us to analyze the whole system as one unit and thus miss many corner cases, which arise due to the operation of all the sub-components of the system together. One of the major concerns is that, despite the above-mentioned evident limitation in the analysis methods, many safety-critical systems, such as aerospace, smart-transportation, smart-grid and e-health, are increasingly involving physical elements. Moreover, we are moving towards integrating more complex physical elements in our engineering systems. For example, we are moving towards Quantum Computers to meet the high performance needs. Similarly, phonic components are increasingly being advocated and used in aerospace applications due to their lightweight and temperature independency compared to traditional electronics based components. Finally, the impact of physical components is relevant to both safety and security of the overall system. For example, malfunction in sensor measurement may lead to safety issues whereas sophisticated physics based side-channel (e.g., power and acoustic measurements) attacks lead to the security violation of the underlying system.
>
> The objective of the workshop is to gather scientists and engineers interested in formal verification techniques for the modeling, analysis and verification of safety and security critical physical systems. We encourage submissions on interdisciplinary approaches that bring together formal methods and techniques from other knowledge areas such as quantum computing, control theory, biology, optimization theory and artificial intelligence.

============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
archives back to 2003: http://friam.471366.n2.nabble.com/
FRIAM-COMIC http://friam-comic.blogspot.com/ by Dr. Strangelove
uǝʃƃ ⊥ glen
Reply | Threaded
Open this post in threaded view
|

Re: FVPS 2019

Steve Smith

Glen -

It does look very interesting.   I think I've referenced THIS (inter-reality) work before:

https://arxiv.org/abs/physics/0611293

as well as the Phononic quantum computing my nephew has been working on.

https://www.technologyreview.com/s/428844/how-to-build-a-phononic-computer/

where classical meets quantum in a more *obvious* way than usual.

it *does* seem that the mismatch of modeling paradigms between science and engineering and often even different domains of either as they converge is a fundamental problem for modelers and simulants and the projects they work on.

I was recently at NREL working with them on the Visualization of Uncertainty which is naturally grounded in the Quantification of Uncertainty which requires some understanding of the Qualities of Uncertainty (e.g. Aleotoric, Epistimic, Ontological) and exposes the many ways one can make mistakes in trying to compound or resolve different types of uncertainties (or errors) against one another.

NREL (and my colleague there) do a LOT of blending/combining of models and are fortunately very sensitive to these issues, whereas many people approaching this for the first time can be rather naive in the way they mash things together.

My first professional job was in developing control systems for a Proton Storage Ring.  The folks on the task were *highly* aware of the problems of coupling digital and analog systems, though mostly focused on the obvious problems with sampling continuous phenomena.   This was 1981 so there were a lot fewer digital components and digital performance was a tiny fraction of what  it is today, leading to more thoughtful care (I contend).

- Steve

On 4/11/19 8:35 AM, glen∈ℂ wrote:
Arg!  I wish I could go to this.  If any of you do, please send along some notes.

2nd Workshop on Formal Verification of Physical Systems (FVPS 2019)
https://www.cicm-conference.org/2019/cicm.php?event=fvps&menu=general

Theme

One of the main issues behind many failing systems is the ad-hoc verification approach that involves a variety of formalism and techniques for the modeling and analysis of various components of the present-age (cyber)-physical systems. For example, control and communication protocols are usually modeled using automata theory, and thus analyzed using model checking techniques, while the modeling of physical aspects often require multivariate calculus foundations, which are in turn analyzed using paper-and-pencil based analytical proofs, simulation or theorem proving. The fundamental differences between these modeling and analysis techniques limit us to analyze the whole system as one unit and thus miss many corner cases, which arise due to the operation of all the sub-components of the system together. One of the major concerns is that, despite the above-mentioned evident limitation in the analysis methods, many safety-critical systems, such as aerospace, smart-transportati!
on, smart-grid and e-health, are increasingly involving physical elements. Moreover, we are moving towards integrating more complex physical elements in our engineering systems. For example, we are moving towards Quantum Computers to meet the high performance needs. Similarly, phonic components are increasingly being advocated and used in aerospace applications due to their lightweight and temperature independency compared to traditional electronics based components. Finally, the impact of physical components is relevant to both safety and security of the overall system. For example, malfunction in sensor measurement may lead to safety issues whereas sophisticated physics based side-channel (e.g., power and acoustic measurements) attacks lead to the security violation of the underlying system.

The objective of the workshop is to gather scientists and engineers interested in formal verification techniques for the modeling, analysis and verification of safety and security critical physical systems. We encourage submissions on interdisciplinary approaches that bring together formal methods and techniques from other knowledge areas such as quantum computing, control theory, biology, optimization theory and artificial intelligence.

============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
archives back to 2003: http://friam.471366.n2.nabble.com/
FRIAM-COMIC http://friam-comic.blogspot.com/ by Dr. Strangelove

============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
archives back to 2003: http://friam.471366.n2.nabble.com/
FRIAM-COMIC http://friam-comic.blogspot.com/ by Dr. Strangelove