Independent procedures that are used together for checking that a product, service, or system meets requirements and specifications and that it fulfills its intended purpose.
Project
CPS: Synergy: Collaborative Research: In-Silico Functional Verification of Artificial Pancreas Control Algorithms
The project investigates a formal verification framework for artificial pancreas (AP) controllers that automate the delivery of insulin to patients with type-1 diabetes (T1D). AP controllers are safety critical: excessive insulin delivery can lead to serious, potentially fatal, consequences. The verification framework under development allows designers of AP controllers to check that their control algorithms will operate safely and reliably against large disturbances that include patient meals, physical activities, and sensor anomalies including noise, delays, and sensor attenuation. The intellectual merits of the project lie in the development of state-of-the-art formal verification tools, that reason over mathematical models of the closed-loop including external disturbances and insulin-glucose response. These tools perform an exhaustive exploration of the closed loop system behaviors, generating potentially adverse situations for the control algorithm under verification. In addition, automatic techniques are being investigated to help AP designers improve the control algorithm by tuning controller parameters to eliminate harmful behaviors and optimize performance. The broader significance and importance of the project are to minimize the manual testing effort for AP controllers, integrate formal tools in the certification process, and ultimately ensure the availability of safe and reliable devices to patients with type-1 diabetes. The framework is made available to researchers who are developing AP controllers to help them verify and iteratively improve their designs. The team is integrating the research into the educational mission by designing hands-on courses to train undergraduate students in the science of Cyber-Physical Systems (CPS) using the design of AP controllers as a motivating example. Furthermore, educational material that explains the basic ideas, current challenges and promises of the AP concept is being made available to a wide audience that includes patients with T1D, their families, interested students, and researchers. The research is being carried out collaboratively by teams of experts in formal verification for Cyber-Physical Systems, control system experts with experience designing AP controllers, mathematical modeling experts, and clinical experts who have clinically evaluated AP controllers. To enable the construction of the verification framework from the current state-of-the-art verification tools, the project is addressing major research challenges, including (a) building plausible mathematical models of disturbances from available clinical datasets characterizing human meals, activity patterns, and continuous glucose sensor anomalies. The resulting models are integrated in a formal verification framework; (b) simplifying existing models of insulin glucose response using smaller but more complex delay differential models; (c) automating the process of abstracting the controller implementation for the purposes of verification; (d) producing verification results that can be interpreted by control engineers and clinical researchers without necessarily understanding formal verification techniques; and (e) partially automating the process of design improvements to potentially eliminate severe faults and improve performance. The framework is evaluated on a set of promising AP controller designs that are currently under various stages of clinical evaluation.
1446900
Off
University of Colorado at Boulder
Sriram Sankaranarayanan
-
National Science Foundation
http://www.nsf.gov/awardsearch/showAward?AWD_ID=1446900&HistoricalAwards=false
Sriram Sankaranarayanan
Sriram Sankaranarayanan Submitted by Sriram Sankaranarayanan on August 27th, 2015
Project
CAREER: Robustness Guided Testing and Verification for Cyber-Physical Systems
This project develops a theoretical framework as well as software tools to support testing and verification of a Cyber-Physical System (CPS) within a Model-Based Design (MBD) process. The theoretical bases of the framework are stochastic optimization methods, and robustness notions of formal specification languages. The project's research comprises three components: development of conditions on the algorithms and on the structure of the CPS for inferring finite-time guarantees on the randomized testing process; the study of testing methods that can support modular and compositional system design; and investigation of appropriate notions of conformance between two system models and between a model and its implementation on a computational platform. All of these components are needed to support testing and verification in all the stages of an MBD process as well as to support component reuse, incremental system improvements and modular design. The evaluation of the framework is driven by the problems of verifying automotive control systems and medical devices. As safety-critical CPS become ubiquitous, the need for design methods that guarantee correct system functionality and performance becomes more urgent. Certification and government agencies need dependable testing and verification tools to incorporate in certification standards and procedures. The concrete benefits to the society are both in terms of reduced catastrophic design errors in new products and in terms of reduced economic costs for new product development. The former increases the confidence in new technologies while the latter improves the competitiveness of the companies that utilize such technologies. The theoretical results of this project are being incorporated into software tools for testing, verification and validation of complex CPS. The evaluation focus of the project on verifying infusion pumps and automotive control software ultimately helps in avoiding harmful losses due to errors in these safety-critical systems. The use of any software tool that is based on formal or semi-formal methods requires engineers with solid training on these technologies. This proposal puts forward an education curriculum for developing new courses that introduce formal and semi-formal methods for CPS at all levels of higher education, i.e., undergraduate, graduate and continuing education. Particular attention is devoted into on-line continuing education of practicing engineers who must acquire new MBD skills.
1350420
Off
Georgios Fainekos
-
National Science Foundation
http://www.nsf.gov/awardsearch/showAward?AWD_ID=1350420&HistoricalAwards=false
Georgios Fainekos
Georgios Fainekos Submitted by Georgios Fainekos on August 27th, 2015
Project
CPS: Synergy: Collaborative Research: Trustworthy Composition of Dynamic App-Centric Architectures for Medical Application Platforms
This project aims to achieve key technology, infrastructure, and regulatory science advances for next generation medical systems based on the concept of medical application platforms (MAPs). A MAP is a safety/security-critical real-time computing platform for: (a) integrating heterogeneous devices and medical IT systems, (b) hosting application programs ("apps") that provide medical utility through the ability to both acquire information and update/control integrated devices, IT systems, and displays. The project will develop formal architectural and behavioral specification languages for defining MAPs, with a focus on techniques that enable compositional reasoning about MAP component interoperability and safety. These formal languages will include an extensible property language to enable the specification of real-time, quality-of-service, and attributes specific to medical contexts that can be leveraged by code generation, testing, and verification tools. The project will work closely with a synergistic team of clinicians, device industry partners, regulators, and medical device interoperability and safety standard organizations to develop an open source MAP innovation platform to enable key stakeholders within the nation's health care ecosphere to identify, prototype, and evaluate solutions to key technology and regulatory challenges that must be overcome to develop a commodity market of regulated MAP components. Because MAPs provide pre-built certified infrastructure and building blocks for rapidly developing multi-device medical applications, this research has the potential to usher in a new paradigm of medical system that significantly increases the pace of innovation, lowers development costs, enables new functionality by aggregating multiple devices into a system of systems, and achieves greater system safety.
1239534
Off
Kansas State University
John Hatcliff
-
National Science Foundation
http://www.nsf.gov/awardsearch/showAward?AWD_ID=1239543&HistoricalAwards=false
Venkatesh Ranganath
John Hatcliff
John Hatcliff Submitted by John Hatcliff on August 27th, 2015
Project
CAREER: Domain-Specific Modeling Techniques for Cyber-Physical Systems

The objective of this research is an injection of new modeling techniques into the area of Cyber-Physical Systems (CPSs). The approach is to design new architectures for domain-specific modeling tools in order to permit feedback from analysis, validation, and verification engines to influence how CPSs are designed. This project involves new research into the integration of existing, heterogeneous modeling languages in order to address problems in CPS design, rather than a single language for all CPS. Since many tools for analysis, validation, and verification focus on at most two of the three major components of CPS (communication, computation, and control), new paradigms in modeling are used to integrate tools early in the design process. The algorithms and software developed in this project run validation and verification tools on models, and then close the loop by using the tool outputs to automatically modify the system models. The satisfaction of design requirements in CPSs is critical for tomorrow's societal technologies such as smart buildings, home healthcare, and water management. Among the most compelling design requirements are those of safety, and CPSs for autonomous vehicles exemplify this well. By involving a full-sized autonomous vehicle in this project, the validation and verification of safety requirements is tied to a concrete platform that is broadly understood. By involving students in the design of behaviors of the vehicle, the project exposes scientists and engineers of tomorrow to societal-scale problems, and tools to address them.

1253334
Off
Loukas Lazos
http://csl.arizona.edu/career
-
National Science Foundation
http://www.nsf.gov/awardsearch/showAward?AWD_ID=1253334&HistoricalAwards=false
Jonathan Sprinkle (Former PI)
Jonathan Sprinkle
Submitted by Loukas Lazos on August 27th, 2015
Event
CRTS 2015
8th International Workshop on Compositional Theory and Technology for Real-Time Embedded Systems (CRTS 2015) Collocated with RTSS 2015. San Antonio TX. USA
Submitted by Anonymous on August 25th, 2015
Event
SCOPES 2016
19th International Workshop on Software and Compilers for Embedded Systems (SCOPES 2016) A next edition of the workshop on Software and Compilers for Embedded Systems  (SCOPES) will be organized in 2016. The workshop will feature a combination of research papers and research presentations (details see below). The papers and presentation abstracts will also be published in the ACM digital library. The workshop is held in cooperation with ACM SIGBED and EDAA. AIM AND SCOPE
Submitted by Anonymous on August 25th, 2015
Event
ARD2016
FIRST CALL FOR PAPERS ARC2016: 12th International Symposium on Applied Reconfigurable Computing    21-24 March 2016 | Mangaratiba, Rio de Janeiro, Brazil |   http://lcr.icmc.usp.br/arc2016/
Submitted by Anonymous on August 25th, 2015
Event
ETAPS 2016
ETAPS is a confederation of several conferences, each with its own Programme Committee and Steering Committee. ETAPS is the most important and visible annual European event related to software sciences. Altogether, more than 500 researchers participate in this event every year.
Submitted by Anonymous on August 25th, 2015
Announcement
Extended Deadline: Integrated Formal Methods iFM 2016, Reykjavik,Iceland: 3rd Call for Workshops

12th International Conference on integrated Formal Methods (FM 2016) 

http://ifm2016.ru.is | June 1-5, 2016 - Reykjavik, Iceland

CALL FOR AFFILIATED WORKSHOPS

Prospective workshop organizers are invited to submit proposals for workshops to be affiliated to iFM 2016, on topics related to the conferences main subjects.

Important Dates

  • Submission of workshop proposals: by September 21, 2015 (extended)
  • Notification: by Oktober 5, 2015 (extended)
  • Workshops: June 4-5, 2015

Submission via e-mail
Marcel Kyas <marcel@ru.is> - Workshop chair

About iFM

iFM 2016 is concerned with how the application of formal methods may involve modelling different aspects of a system which are best expressed using different formalisms. Correspondingly, different analysis techniques may be used to examine different system views, different kinds of properties, or simply in order to cope with the sheer complexity of the system. The iFM conference series seeks to further research into hybrid approaches to formal modelling and analysis; i.e., the combination of (formal and semi-formal) methods for system development, regarding modelling and analysis, and covering all aspects from language design through verification and analysis techniques to tools and their integration into software engineering practice.

One day workshops will be held in conjunction with the main events.
Prospective workshop organizers are requested to follow the guidelines below and are encouraged to contact the workshop chairs if any questions arise.

The following speakers are invited to iFM2016:

  • Marsha Chechik (University of Toronto, Canada)
  • Edmund M. Clarke (Carnegie Mellon University, USA)
  • Laura Kovács (Chalmers University of Technology, Sweden)
  • Reiner Hähnle (Technical University Darmstadt, Germany)

The purpose of the workshops is to provide participants with a friendly, interactive atmosphere for presenting novel ideas and discussing their application.

The workshops take place on June 4-5, 2016.

Proposal and Submission Guidelines

Workshop proposals must be written in English, not exceed 5 pages with a reasonable font and margins, and be submitted in PDF format via email to Marcel Kyas (marcel@ru.is).

Proposals should include:

  • The name and the preferred date of the proposed workshop
  • A short description of the workshop.
  • If applicable, a description of past versions of the workshop, including dates, organizers, submission and acceptance counts, and attendance.
  • The publicity strategy that will be used by the workshop organizers to promote the workshop.
  • The participant solicitation and selection process.
  • The target audience and expected number of participants.
  • Approximate budget proposal (see section Budget below for details).
  • The equipment and any other resource necessary for the organization of the workshop.
  • The name and short CV of the organizer(s).
  • The publication plan (only invited speakers, no published proceedings, pre-/post-proceedings published with EPTCS/ENTCS/...)

Organizers Responsibilities

The scientific responsibility of organizing a workshop goes to the workshop organizers. In particular, they are responsible for the following items:

  • A workshop description (200 words) for inclusion n the iFM site.
  • Hosting and maintaining web pages to be linked from the iFM site. Workshop organizers can integrate their pages into the main iFM pages.
  • Workshop proceedings, if any. If there is sufficient interest, the organizer of iFM 2016 may contact the editor-in-chief of the Electronic Proceedings in Theoretical Computer Science (http://info.eptcs.org/) for having a common volume dedicated to the workshops of iFM 2016.
  • Workshop publicity (possibly including call for papers, submission and review process).
  • Scheduling workshop activities in collaboration with the iFM workshop chair.

If you intend to organize a workshop but you need more time to prepare your proposal please let us know.

Please note that as the number of tourists travelling to Iceland in summer time is exceeding its population, we need to know the number of participants before March 23 to be able to reserve accommodation. We cannot guarantee accomodation for participants that register after March 23.

Budget

The iFM organization will provide registration and organizational support for the workshops (including link from the conferences web sites, set-up of meeting space, on-line and on-site registration). Registration fees must be paid for all participants, including organizers and invited guests.

To cover lunches, coffee breaks and basic organizational expenses, all workshops will be required to charge a minimum participation fee (the precise amount is still to be determined). Each workshop may increase this fee to cover additional expenses such as publication charges, student scholarships, costs for invited speakers, etc. All fees will be collected by the iFM organizers as part of the registration, then additional funds will be redistributed to the individual workshop organizers.

Evaluation Process

The proposals will be evaluated by the iFM organizing committee on the basis of their assessed benefit for prospective participants of iFM 2016. Prospective organizers may wish to consult the web pages of previous satellite events as examples:

  • iFM 2014: http://ifm2014.cs.unibo.it/workshops.html
  • iFM 2013: http://www.it.abo.fi/iFM2013/workshops_and_tutorials.php
  • iFM 2012: http://ifm-abz.isti.cnr.it/styled-4/speakers.html
  • iFM 2010: http://ifm2010.loria.fr/satellite.html
  • iFM 2009: http://www.formal-methods.de/ifm09/workshops.html

Venue

iFM 2016 will take place at the Campus of Reykjavik University, Iceland. The campus at Reykjavik University is set in one of the most beautiful areas next to Iceland's only geothermal beach. The building has well equipped classrooms.

Further Information and Enquiries

Please contact the workshop chair Marcel Kyas <marcel@ru.is>

General Announcement
Not in Slideshow
Submitted by Anonymous on August 25th, 2015
Event
(MC)3
Multi-Core and Many-Core systems for EMbedded Computing (MC)3 Special session in 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2016) http://www.pdp2016.org/SS9.html 17-19 Feb. 2016, Crete, Greece
Submitted by Anonymous on August 10th, 2015
Subscribe to Validation and Verification