Search

Verification of asynchronous distributed programs is challenging due to the need to reason about numerous control paths resulting from the myriad interleaving of messages and failures. In this paper, we propose an automated bookkeeping method based on message chains. Message chains reveal structure in asynchronous distributed system executions and can help programmers verify their systems at the message passing level of abstraction. To evaluate our contributions empirically we build a verification prototype for the P programming language that integrates message chains. We use it to verify 16 benchmarks from related work, one new benchmark that exemplifies the kinds of systems our method focuses on, and two industrial benchmarks. We find that message chains are able to simplify existing proofs and our prototype performs comparably to existing work in terms of runtime. We extend our work with support for specification mining and find that message chains provide enough structure to allow existing learning and program synthesis tools to automatically infer meaningful specifications using only execution examples.

Background Diabetes control is poor globally and leads to burdensome microvascular and macrovascular complications. We aimed to assess post hoc between-group differences in sustained risk factor control and macrovascular and microvascular endpoints at 6.5 years in the Center for cArdiovascular Risk Reduction in South Asia (CARRS) randomized trial. Methods and findings This parallel group individual randomized clinical trial was performed at 10 outpatient diabetes clinics in India and Pakistan from January 2011 through September 2019. A total of 1,146 patients with poorly controlled type 2 diabetes (HbA1c [greater than or equal to]8% and systolic BP [greater than or equal to]140 mm Hg and/or LDL-cholesterol [greater than or equal to]130 mg/dL) were randomized to a multicomponent quality improvement (QI) strategy (trained nonphysician care coordinator to facilitate care for patients and clinical decision support system for physicians) or usual care. At 2.5 years, compared to usual care, those receiving the QI strategy were significantly more likely to achieve multiple risk factor control. Six clinics continued, while 4 clinics discontinued implementing the QI strategy for an additional 4-year follow-up (overall median 6.5 years follow-up). In this post hoc analysis, using intention-to-treat, we examined between-group differences in multiple risk factor control (HbA1c Conclusions In urban South Asian clinics, a multicomponent QI strategy led to sustained multiple risk factor control and between-group differences in microvascular, but not macrovascular, endpoints. Between-group reductions in vascular outcomes at 6.5 years were observed only at sites that continued the QI intervention, suggesting that practice change needs to be maintained for better population health of people with diabetes. Trial registration ClinicalTrials.gov NCT01212328., Author(s): Mohammed K. Ali 1,2, Kavita Singh 3,4, Dimple Kondal 5, Raji Devarajan 4, Shivani A. Patel 1,2,6, V. Usha Menon 7, Premlata K. Varthakavi 8, Vijay Vishwanathan 9, Mala [...]

The recent drive towards achieving greater autonomy and intelligence in robotics has led to high levels of complexity. Autonomous robots increasingly depend on third-party off-The-shelf components and complex machine-learning techniques. This trend makes it challenging to provide strong design-Time certification of correct operation. To address these challenges, we present SOTER, a robotics programming framework with two key components: (1) a programming language for implementing and testing high-level reactive robotics software, and (2) an integrated runtime assurance (RTA) system that helps enable the use of uncertified components, while still providing safety guarantees. SOTER provides language primitives to declaratively construct a RTA module consisting of an advanced, high-performance controller (uncertified), a safe, lower-performance controller (certified), and the desired safety specification. The framework provides a formal guarantee that a well-formed RTA module always satisfies the safety specification, without completely sacrificing performance by using higher performance uncertified components whenever safe. SOTER allows the complex robotics software stack to be constructed as a composition of RTA modules, where each uncertified component is protected using a RTA module. To demonstrate the efficacy of our framework, we consider a real-world case-study of building a safe drone surveillance system. Our experiments both in simulation and on actual drones show that the SOTER-enabled RTA ensures the safety of the system, including when untrusted third-party components have bugs or deviate from the desired behavior.

A real-world distributed system is rarely implemented as a standalone monolithic system. Instead, it is composed of multiple independent interacting components that together ensure the desired system-level specification. One can scale systematic testing to large, industrial-scale implementations by decomposing the system-level testing problem into a collection of simpler component-level testing problems. This paper proposes techniques for compositional programming and testing of distributed systems with two central contributions: (1) We propose a module system based on the theory of compositional trace refinement for dynamic systems consisting of asynchronously-communicating state machines, where state machines can be dynamically created, and communication topology of the existing state machines can change at runtime; (2) We present ModP, a programming system that implements our module system to enable compositional reasoning (assume-guarantee) of distributed systems. We demonstrate the efficacy of our framework by building two practical fault-tolerant distributed systems, a transaction-commit service and a replicated hash-table. ModP helps implement these systems modularly and validate them via compositional testing. We empirically demonstrate that the abstraction-based compositional reasoning approach helps amplify the coverage during testing and scale it to real-world distributed systems. The distributed services built using ModP achieve performance comparable to open-source equivalents.

The increasing use of deep neural networks in a variety of applications, including some safety-critical ones, has brought renewed interest in the topic of verification of neural networks. However, verification is most meaningful when performed with high-quality formal specifications. In this paper, we survey the landscape of formal specification for deep neural networks, and discuss the opportunities and challenges for formal methods for this domain.

Distributed mobile robotics (DMR) involves teams of networked robots navigating in a physical space to achieve tasks in a coordinated fashion. A major challenge in DMR is to program the ensemble of robots with formal guarantees and high assurance of correct operation. To this end, we introduce Drona, a framework for building reliable DMR applications. This paper makes three central contributions: (1) We present a novel and provably correct decentralized asynchronous motion planner that can perform on-the-fly collision-free planning for dynamically generated tasks. Moreover, the motion planner is the first to take into account the fact that distributed robots may have clocks that are only synchronized up to a tolerance, i.e., they are almost synchronous; (2) We formalize the DMR system as a mixed-synchronous system, and present a sound abstraction-based verification approach for DMR systems, and (3) Drona provides a state-machine based language for safe event-driven programming of a DMR system and the code generated by the compiler can be executed on platforms such as the robot operating system (ROS). To demonstrate the efficacy of Drona, we build and verify a priority mail delivery system. Using our abstraction-based verification approach we were able to find, within a few minutes, bugs which could not be found by performing random simulation for several hours. Our verified decentralized motion-planner scales efficiently for large number of robots (upto 128 robots) and workspace sizes (upto a 256×256 grid).

A major challenge towards large scale deployment of autonomous mobile robots is to program them with formal guarantees and high assurance of correct operation. To this end, we present a framework for building safe robots. Our approach for validating the end-to-end correctness of robotics system consists of two parts: (1) a high-level programming language for implementing and systematically testing the reactive robotics software via model checking; (2) a signal temporal logic (STL) based online monitoring system to ensure that the assumptions about the low-level controllers (discrete models) used during model checking hold at runtime. Combining model checking with runtime verification helps us bridge the gap between software verification (discrete) that makes assumptions about the low-level controllers and the physical world, and the actual execution of the software on a real robotic platform in the physical world. To demonstrate the efficacy of our approach, we build a safe adaptive surveillance system and present software-in-the-loop simulations of the application.

Forms of synchrony can greatly simplify modeling, design, and verification of distributed systems. Thus, recent advances in clock synchronization protocols and their adoption hold promise for system design. However, these protocols synchronize the distributed clocks only within a certain tolerance, and there are transient phases while synchronization is still being achieved. Abstractions used for modeling and verification of such systems should accurately capture these imperfections that cause the system to only be “almost synchronized.” In this paper, we present approximate synchrony, a sound and tunable abstraction for verification of almost-synchronous systems. We show how approximate synchrony can be used for verification of both time synchronization protocols and applications running on top of them. We provide an algorithmic approach for constructing this abstraction for symmetric, almost-synchronous systems, a subclass of almost-synchronous systems. Moreover, we show how approximate synchrony also provides a useful strategy to guide state-space exploration. We have implemented approximate synchrony as a part of a model checker and used it to verify models of the Best Master Clock (BMC) algorithm, the core component of the IEEE 1588 precision time protocol, as well as the time-synchronized channel hopping protocol that is part of the IEEE 802.15.4e standard.

This paper studies conditions where messages endlessly circulate in a system of IEEE 1588-2008 clocks. The study is based on two independent analysis techniques. One uses a discrete event simulation environment for describing the operation of the best master clock (BMC) algorithm in IEEE 1588-2008. The second uses a model checking tool. We discuss several cases illustrating conditions under which circulating messages occur and the effectiveness of measures to squelch these messages. This paper demonstrates that one or more of the squelching mechanisms must be implemented.

Objectives: To explore associations between type and number of abnormal glucose values on antenatal oral glucose tolerance test (OGTT) with postpartum diabetes in South Asian women diagnosed with gestational diabetes (GDM) using International Association of the Diabetes and Pregnancy Study Groups criteria. Methods: This post‐hoc evaluation of the Lifestyle Intervention IN Gestational Diabetes (LIVING) study, a randomized controlled trial, was conducted among women with GDM in the index pregnancy, across 19 centers in Bangladesh, India, and Sri Lanka. Postpartum diabetes (outcome) was defined on OGTT, using American Diabetes Association (ADA) criteria. Results: We report data on 1468 women with GDM, aged 30.9 (5.0) years, and with median (interquartile range) follow‐up period of 1.8 (1.4–2.4) years after childbirth following the index pregnancy. We found diabetes in 213 (14.5%) women with an incidence of 8.7 (7.6–10.0)/100 women‐years. The lowest incidence rate was 3.8/100 women years, in those with an isolated fasting plasma glucose (FPG) abnormality, and highest was 19.0/100 women years in participants with three abnormal values. The adjusted hazard ratios for two and three abnormal values compared to one abnormal value were 1.73 (95% confidence interval [CI], 1.18–2.54; p =.005) and 3.56 (95% CI, 2.46–5.16; p <.001) respectively. The adjusted hazard ratio for the combined (combination of fasting and postglucose load) abnormalities was 2.61 (95% CI, 1.70–4.00; p <.001), compared to isolated abnormal FPG. Conclusions: Risk of diabetes varied significantly depending upon the type and number of abnormal values on antenatal OGTT. These data may inform future precision medicine approaches such as risk prediction models in identifying women at higher risk and may guide future targeted interventions. [ABSTRACT FROM AUTHOR]