@inproceedings{1103,
abstract = {We propose two parallel state-space-exploration algorithms for hybrid automaton (HA), with the goal of enhancing performance on multi-core shared-memory systems. The first uses the parallel, breadth-first-search algorithm (PBFS) of the SPIN model checker, when traversing the discrete modes of the HA, and enhances it with a parallel exploration of the continuous states within each mode. We show that this simple-minded extension of PBFS does not provide the desired load balancing in many HA benchmarks. The second algorithm is a task-parallel BFS algorithm (TP-BFS), which uses a cheap precomputation of the cost associated with the post operations (both continuous and discrete) in order to improve load balancing. We illustrate the TP-BFS and the cost precomputation of the post operators on a support-function-based algorithm for state-space exploration. The performance comparison of the two algorithms shows that, in general, TP-BFS provides a better utilization/load-balancing of the CPU. Both algorithms are implemented in the model checker XSpeed. Our experiments show a maximum speed-up of more than 2000 χ on a navigation benchmark, with respect to SpaceEx LGG scenario. In order to make the comparison fair, we employed an equal number of post operations in both tools. To the best of our knowledge, this paper represents the first attempt to provide parallel, reachability-analysis algorithms for HA.},
author = {Gurung, Amit and Deka, Arup and Bartocci, Ezio and Bogomolov, Sergiy and Grosu, Radu and Ray, Rajarshi},
location = {Kanpur, India },
publisher = {IEEE},
title = {{Parallel reachability analysis for hybrid systems}},
doi = {10.1109/MEMCOD.2016.7797741},
year = {2016},
}
@phdthesis{1130,
abstract = {In this thesis we present a computer-aided programming approach to concurrency. Our approach
helps the programmer by automatically fixing concurrency-related bugs, i.e. bugs that occur
when the program is executed using an aggressive preemptive scheduler, but not when using a
non-preemptive (cooperative) scheduler. Bugs are program behaviours that are incorrect w.r.t.
a specification. We consider both user-provided explicit specifications in the form of assertion
statements in the code as well as an implicit specification. The implicit specification is inferred
from the non-preemptive behaviour. Let us consider sequences of calls that the program makes
to an external interface. The implicit specification requires that any such sequence produced
under a preemptive scheduler should be included in the set of sequences produced under a
non-preemptive scheduler.
We consider several semantics-preserving fixes that go beyond atomic sections typically
explored in the synchronisation synthesis literature. Our synthesis is able to place locks, barriers
and wait-signal statements and last, but not least reorder independent statements. The latter
may be useful if a thread is released to early, e.g., before some initialisation is completed. We
guarantee that our synthesis does not introduce deadlocks and that the synchronisation inserted
is optimal w.r.t. a given objective function.
We dub our solution trace-based synchronisation synthesis and it is loosely based on
counterexample-guided inductive synthesis (CEGIS). The synthesis works by discovering a
trace that is incorrect w.r.t. the specification and identifying ordering constraints crucial to trigger
the specification violation. Synchronisation may be placed immediately (greedy approach) or
delayed until all incorrect traces are found (non-greedy approach). For the non-greedy approach
we construct a set of global constraints over synchronisation placements. Each model of the
global constraints set corresponds to a correctness-ensuring synchronisation placement. The
placement that is optimal w.r.t. the given objective function is chosen as the synchronisation
solution.
We evaluate our approach on a number of realistic (albeit simplified) Linux device-driver
benchmarks. The benchmarks are versions of the drivers with known concurrency-related bugs.
For the experiments with an explicit specification we added assertions that would detect the bugs
in the experiments. Device drivers lend themselves to implicit specification, where the device and
the operating system are the external interfaces. Our experiments demonstrate that our synthesis
method is precise and efficient. We implemented objective functions for coarse-grained and
fine-grained locking and observed that different synchronisation placements are produced for
our experiments, favouring e.g. a minimal number of synchronisation operations or maximum
concurrency.},
author = {Tarrach, Thorsten},
pages = {151},
publisher = {IST Austria},
title = {{Automatic synthesis of synchronisation primitives for concurrent programs}},
year = {2016},
}
@inproceedings{1134,
abstract = {Hybrid systems have both continuous and discrete dynamics and are useful for modeling a variety of control systems, from air traffic control protocols to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools for analyzing hybrid systems have emerged. Several of these tools implement automated formal methods for mathematically proving a system meets a specification. This tutorial session will present three recent hybrid systems tools: C2E2, HyST, and TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses validated numerical solvers and bloating of simulation traces to verify systems meet specifications. HyST is a hybrid systems model transformation and translation tool, and uses a canonical intermediate representation to support most of the recent verification tools, as well as automated sound abstractions that simplify verification of a given hybrid system. TuLiP is a controller synthesis tool for hybrid systems, where given a temporal logic specification to be satisfied for a system (plant) model, TuLiP will find a controller that meets a given specification. © 2016 IEEE.},
author = {Duggirala, Parasara and Fan, Chuchu and Potok, Matthew and Qi, Bolun and Mitra, Sayan and Viswanathan, Mahesh and Bak, Stanley and Bogomolov, Sergiy and Johnson, Taylor and Nguyen, Luan and Schilling, Christian and Sogokon, Andrew and Tran, Hoang and Xiang, Weiming},
booktitle = {2016 IEEE Conference on Control Applications},
location = {Buenos Aires, Argentina },
publisher = {IEEE},
title = {{Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP}},
doi = {10.1109/CCA.2016.7587948},
year = {2016},
}
@inproceedings{1135,
abstract = {Time-triggered (TT) switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. These networks rely on the notion of globally discretized time (i.e. time slots) and a static TT schedule that prescribes which message is sent through which link at every time slot, such that all messages reach their destination before a global timeout. These schedules are generated offline, assuming a static network with fault-free links, and entrusting all error-handling functions to the end user. Assuming the network is static is an over-optimistic view, and indeed links tend to fail in practice. We study synthesis of TT schedules on a network in which links fail over time and we assume the switches run a very simple error-recovery protocol once they detect a crashed link. We address the problem of finding a pk; qresistant schedule; namely, one that, assuming the switches run a fixed error-recovery protocol, guarantees that the number of messages that arrive at their destination by the timeout is at least no matter what sequence of at most k links fail. Thus, we maintain the simplicity of the switches while giving a guarantee on the number of messages that meet the timeout. We show how a pk; q-resistant schedule can be obtained using a CEGAR-like approach: find a schedule, decide whether it is pk; q-resistant, and if it is not, use the witnessing fault sequence to generate a constraint that is added to the program. The newly added constraint disallows the schedule to be regenerated in a future iteration while also eliminating several other schedules that are not pk; q-resistant. We illustrate the applicability of our approach using an SMT-based implementation. © 2016 ACM.},
author = {Avni, Guy and Guha, Shibashis and Rodríguez Navas, Guillermo},
booktitle = {Proceedings of the 13th International Conference on Embedded Software },
location = {Pittsburgh, PA, USA},
publisher = {ACM},
title = {{Synthesizing time triggered schedules for switched networks with faulty links}},
doi = {10.1145/2968478.2968499},
year = {2016},
}
@inproceedings{1138,
abstract = {Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider. © 2016 ACM.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan},
booktitle = {Proceedings of the 31st Annual ACM/IEEE Symposium},
location = {New York, NY, USA},
pages = {76 -- 85},
publisher = {IEEE},
title = {{Quantitative automata under probabilistic semantics}},
doi = {10.1145/2933575.2933588},
year = {2016},
}