Model-checking web services business activity protocolsInternational Journal on Software Tools for Technology Transfer - Tập 15 - Trang 125-147 - 2012
Abinoam P. Marques, Anders P. Ravn, Jiří Srba, Saleem Vighio
Web services business activity (WS-BA) specification defines two coordination protocols BAwCC (Business Agreement with Coordination Completion) and BAwPC (Business Agreement with Participant Completion) that ensure a consistent agreement on the outcome of long-running distributed applications. To verify fundamental properties of the protocols, we provide formal analyses in the model checker Uppaal...... hiện toàn bộ
Verifying a quantitative relaxation of linearizability via refinementInternational Journal on Software Tools for Technology Transfer - Tập 18 - Trang 393-407 - 2015
Kiran Adhikari, James Street, Chao Wang, Yang Liu, Shaojie Zhang
The recent years have seen increasingly widespread use of highly concurrent data structures in both multi-core and distributed computing environments, thereby escalating the priority for verifying their correctness. Quasi linearizability is a quantitative variation of the standard linearizability correctness condition to allow more implementation freedom for performance optimization. However, ensu...... hiện toàn bộ
History, status, and recent trends of the testing and test control notation version 3 (TTCN-3)International Journal on Software Tools for Technology Transfer - Tập 16 Số 3 - Trang 215-225 - 2014
Grabowski, Jens, Schieferdecker, Ina, Ulrich, Andreas
This overview article presents the Testing and Test Control Notation (TTCN-3) success story and serves as an introduction to this Special Section that contains five articles selected from the TTCN-3 user conference in 2011. The article sketches the development of TTCN-3 from its very beginning. It summarizes the current status of the language by reviewing its standardization process, available tes...... hiện toàn bộ
Modelling defence logistics networksInternational Journal on Software Tools for Technology Transfer - - 2008
Guy Edward Gallasch, Nimrod Lilith, Jonathan Billington, Zhang Lin, Axel Bender, Benjamin Francis
Verification of randomized consensus algorithms under round-rigid adversariesInternational Journal on Software Tools for Technology Transfer - Tập 23 - Trang 797-821 - 2021
Nathalie Bertrand, Igor Konnov, Marijana Lazić, Josef Widder
Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We exten...... hiện toàn bộ
Neural predictive monitoring and a comparison of frequentist and Bayesian approachesInternational Journal on Software Tools for Technology Transfer - Tập 23 - Trang 615-640 - 2021
Luca Bortolussi, Francesca Cairoli, Nicola Paoletti, Scott A. Smolka, Scott D. Stoller
Neural state classification (NSC) is a recently proposed method for runtime predictive monitoring of hybrid automata (HA) using deep neural networks (DNNs). NSC trains a DNN as an approximate reachability predictor that labels an HA state x as positive if an unsafe state is reachable from x within a given time bound, and labels x as negative otherwise. NSC predictors have very high accuracy, yet a...... hiện toàn bộ
LearnLib: a framework for extrapolating behavioral modelsInternational Journal on Software Tools for Technology Transfer - Tập 11 - Trang 393-407 - 2009
Harald Raffelt, Bernhard Steffen, Therese Berg, Tiziana Margaria
In this paper, we present the LearnLib, a library of tools for automata learning, which is explicitly designed for the systematic experimental analysis of the profile of available learning algorithms and corresponding optimizations. Its modular structure allows users to configure their own tailored learning scenarios, which exploit specific properties of their envisioned applications. As has been ...... hiện toàn bộ
Don’t care in SMT: building flexible yet efficient abstraction/refinement solversInternational Journal on Software Tools for Technology Transfer - Tập 12 - Trang 23-37 - 2009
Andreas Bauer, Martin Leucker, Christian Schallhart, Michael Tautschnig
This paper describes a method for combining “off-the-shelf” SAT and constraint solvers for building an efficient Satisfiability Modulo Theories (SMT) solver for a wide range of theories. Our method follows the abstraction/refinement approach to simplify the implementation of custom SMT solvers. The expected performance penalty by not using an interweaved combination of SAT and theory solvers is re...... hiện toàn bộ