The purpose of this meeting is to bring together researchers in several fields to develop a coordinated roadmap for computational tools for Cyber-Physical Systems; this meeting will bridge the gap between the hybrid systems community and the validated numerics community. Although both have developed methods for rigorous reasoning about dynamical systems, both faced challenges in making their tools available to practicing engineering. The meeting will focus on two key challenges: scalability and usability.

Cyber-Physical Systems ( CPSs ) [ LS,2011; Marwedel,2011 ] consist of computers that are connected tightly to physical environments through sensors and actuators. Examples of CPSs include robots, smart homes, vehicles, medical implants, and sensor networks.
Mathematically, we can view CPSs as hybrid systems [Alur+,1995] that exhibit both continuous and discrete changes. Many CPSs are also subject to real-time and reactive constraints. CPSs are an engineering, multi-disciplinary area that is rapidly gaining wide acceptance and traction in scientific, social, political, and commercial circles.

Both the hybrid systems community and the validated numerics community have produced formal tools that are important for rigorous design of CPSs.  Reachability analysis of hybrid systems was proposed by the first community as an extension of the model checking method in the context of verification involving continuous quantities. To handle reachable sets of real-valued states, the proposed tools either abstract them into a discrete representation or over-approximate them using numerical objects such as intervals and polytopes. Since the development of interval analysis in 1960’s, validated numerics [Moore,1966; Neumaier,1990] has been used by the second community to produce powerful tools for solving mathematical problems that are formally correct. The achievements include the interval Newton methods, interval Taylor methods [Lohner,1987; MB,2003] , constraint programming techniques [BG,2006; FHRS,2007; GAC,2012] , and inner approximation methods [GMK,2014] .

Unfortunately, CPS designers encounter some challenges with using both reachability analysis and validated numerics. In particular, formal methods often have a steep learning curve that hampers their adoption in industrial practice. It is therefore important to provide tool support for users that fills in gaps in the background knowledge of logic, algebra, real analysis, etc. In the context of reachability analysis of hybrid systems, tools, e.g., HyTech [Alur+,1995] , Uppaal [BDL,2004] , SpaceEx [Frehse+,2011] , have been developed. However, users may still face difficulties in analyzing their problems with these tools. Because each tool depends on the underlying verification algorithm and the form in which hybrid systems are represented, these aspects restrict the tractable class and size of the problems. When a tool does not work immediately, a difficulty lies in what users can do with the tool and with various restrictions in its implementation such as linearity of arithmetic constraints, and support for the description of large systems. Similarly, validated numerics methods today exist mainly in the
form of specialized libraries that are only accessible to experts in this domain. Although integration of the reachability analysis and validated numerics is necessary to push forward the rigorous CPS development, there is still an enormous gap between them [EFH,2008; GMEH,2010; IUH,2011; RN,2011; CAS,2012; BMCP,2012; GKC,2013; GMK,2014].

The central motivation for this Shonan meeting is the prospect that tools based on carefully designed, declarative, high-level modeling formalisms that are natural to the hybrid systems domain can help overcome these challenges [Taha+,2012; UMTHI,2012; SSH,2013; BP,2013; SLMS,2014] .  Such tools allow us to describe models and verification problems in a straightforward manner that is more easily usable by practitioners, and the interpreters transform the model and extract underlying subproblems to which scalable validated numerical methods can be applied. However, designing such tools requires close interdisciplinary cooperation between experts not only in language design but also in hybrid systems, reachability analysis, validated numerics, and practitioners. It seems particularly important and timely to connect the research communities in a way that can be as widely applicable across as many CPS domains as possible. This meeting will bring together researchers working in these areas to better understand these challenges and to develop a common, coordinated vision for addressing them. Expected outcomes include a survey of the state of the art and a roadmap for bridging the gap between the communities.

The organizers will serve as scribes for introduction of the goals of the meeting, the presentations by participants from the above mentioned areas, and the development of a joint roadmap document. An organizer, Walid Taha, has founded several conferences and workshops, including ACM GPCE, SAIG Workshops, and CyPhy workshops on the domain of CPSs. The PC of past CyPhy includes several invitees of this meeting. Another organizer, Kohei Suenaga, has contributed to a past successful Shonan meeting on hybrid systems.