This article provides an innovative approach for verification by model checking of programs that undergo continuous changes. To tackle the problem of repeating the entire model checking for each new version of the program, our approach verifies programs incrementally. It reuses computational history of the previous program version, namely function summaries. In particular, the summaries are over-approximations of the bounded program behaviors. Whenever reusing of summaries is not possible straight away, our algorithm repairs the summaries to maximize the chance of reusability of them for subsequent runs. We base our approach on satisfiability modulo theories (SMT) to take full advantage of lightweight modeling approach and at the same time the ability to provide concise function summarization. Our approach leverages pre-computed function summaries in SMT to localize the checks of changed functions. Furthermore, to exploit the trade-off between precision and performance, our approach relies on the use of an SMT solver, not only for underlying reasoning, but also for program modeling and the adjustment of its precision. On the benchmark suite of primarily Linux device drivers versions, we demonstrate that our algorithm achieves an order of magnitude speedup compared to prior approaches.
- Keywords
- Craig interpolation, Incremental verification, Program changes, SMT solving, Symbolic model checking,
- Publication type
- Journal Article MeSH
MOTIVATION: The problem of model inference is of fundamental importance to systems biology. Logical models (e.g. Boolean networks; BNs) represent a computationally attractive approach capable of handling large biological networks. The models are typically inferred from experimental data. However, even with a substantial amount of experimental data supported by some prior knowledge, existing inference methods often focus on a small sample of admissible candidate models only. RESULTS: We propose Boolean network sketches as a new formal instrument for the inference of Boolean networks. A sketch integrates (typically partial) knowledge about the network's topology and the update logic (obtained through, e.g. a biological knowledge base or a literature search), as well as further assumptions about the properties of the network's transitions (e.g. the form of its attractor landscape), and additional restrictions on the model dynamics given by the measured experimental data. Our new BNs inference algorithm starts with an 'initial' sketch, which is extended by adding restrictions representing experimental data to a 'data-informed' sketch and subsequently computes all BNs consistent with the data-informed sketch. Our algorithm is based on a symbolic representation and coloured model-checking. Our approach is unique in its ability to cover a broad spectrum of knowledge and efficiently produce a compact representation of all inferred BNs. We evaluate the method on a non-trivial collection of real-world and simulated data. AVAILABILITY AND IMPLEMENTATION: All software and data are freely available as a reproducible artefact at https://doi.org/10.5281/zenodo.7688740.
BACKGROUND: It is very difficult to find a consensus that will be accepted by most players when creating health care legislation. The Czech electronic prescription system was launched in 2011 and new functions were introduced in 2018. To ensure that these functions will not conflict with any other existing law, a process modeling tool based on the patent "Method and system for automated requirements modeling" was used successfully in the Czech Republic for the first time. OBJECTIVE: The aim of this project was to develop another successful application of process modeling to add COVID-19 vaccination records to the existing electronic prescription system. METHODS: The method employed was based on the mathematical theory of hierarchical state diagrams and process models. In the first step, sketches that record the results of informal discussions, interviews, meetings, and workshops were prepared. Subsequently, the architecture containing the main participants and their high-level interactions was drafted. Finally, detailed process diagrams were drawn. Each semiresult was discussed with all involved team members and stakeholders to incorporate all comments. By repeating this procedure, individual topics were gradually resolved and the areas of discussion were narrowed down until reaching complete agreement. RESULTS: This method proved to be faster, clearer, and significantly simpler than other methods. Owing to the use of graphic tools and symbols, the risk of errors, inaccuracies, and misunderstandings was significantly reduced. The outcome was used as an annex to the bill in the legislative process. One of the main benefits of this approach is gaining a higher level of understanding for all parties involved (ie, legislators, the medical community, patient organizations, and information technology professionals). The process architecture model in a form of a graphic scheme has proven to be a valuable communication platform and facilitated negotiation between stakeholders. Moreover, this model helped to avoid several inconsistencies that appeared during workshops and discussions. Our method worked successfully even when participants were from different knowledge areas. CONCLUSIONS: The vaccination record process model was drafted in 3 weeks and it took a total of 2 months to pass the bill. In comparison, the initial introduction of the electronic prescription system using conventional legislative methods took over 1 year, involving immediate creation of a text with legislative intent, followed by paragraph-by-section wording of the legislation that was commented on directly. These steps are repeated over and over, as any change in any part of the text has to be checked and rechecked within the entire document. Compared with conventional methods, we have shown that using our method for the process of modification of legislation related to such a complex issue as the integration of COVID-19 vaccination into an electronic prescription model significantly simplifies the preparation of a legislative standard.
- Keywords
- COVID-19, communication, eHealth, electronic prescription, medical, platform, process modeling, state diagram, vaccination, vaccine,
- Publication type
- Journal Article MeSH
The CORAL software ( http://www.insilico.eu/coral ) was used to build up quantitative structure-property relationships (QSPRs) for the retention characteristics of 93 derivatives of three groups of heterocyclic compounds: 2-phenyl-1,3-benzoxazoles, 4-benzylsulfanylpyridines, and benzoxazines. The QSPRs are one-variable models based on the optimal descriptors calculated from the molecular structure represented by simplified molecular input-line entry systems (SMILES). Each symbol (or two undivided symbols) of SMILES is characterized by correlation weight. The optimal descriptor is the sum of the correlation weights. The numerical data on the correlation weights were calculated with the Monte Carlo method by the manner which provides best correlation between endpoint and optimal descriptor for the calibration set. The predictive ability of the model is checked with the validation set (compounds invisible during building up of the model). The approach has been checked with three random splits into the training, calibration, and validation sets: all models have apparent predictive potential. The mechanistic interpretation of the molecular features extracted from SMILES as the promoters of increase or decrease of examined endpoints is suggested.
- Keywords
- CORAL software, Monte Carlo method, QSPR, Retention factor, SMILES,
- Publication type
- Journal Article MeSH
- Research Support, Non-U.S. Gov't MeSH
