Designing safety-critical systems is a complex process, and especially when the design is carried out at different levels of abstraction where the correctness of the design at one level is not ...automatically sustained over the next level. In this work we focus on time-triggered (TT) systems where the resources of communication and computation are shared among different applications to reduce the overall cost of the system. This entails serializing both communication and computation which does not necessarily meet the assumptions made by the application. Hence, we present the concept of executable formal specification of general TT systems to establish a faithful model of the TT characteristics. Our focus is on general applications running in a synchronous environment. The proposed model can be easily customized by the user and it is able to support simulation and verification of the system. It also aids the effective deployment of applications, and the validation of the real system with model-based test generation. Our case study shows how the general model can be implemented in the SAL language and how SAL's tool suite can be used to guidethe design of general TT systems.
We present online tunable diagnostic and membership protocols for generic time-triggered (TT) systems to detect crashes, send/receive omission faults, and network partitions. Compared to existing ...diagnostic and membership protocols for TT systems, our protocols do not rely on the single-fault assumption and also tolerate non-fail-silent (Byzantine) faults. They run at the application level and can be added on top of any TT system (possibly as a middleware component) without requiring modifications at the system level. The information on detected faults is accumulated using a penalty/reward algorithm to handle transient faults. After a fault is detected, the likelihood of node isolation can be adapted to different system configurations, including configurations where functions with different criticality levels are integrated. All protocols are formally verified using model checking. Using actual automotive and aerospace parameters, we also experimentally demonstrate the transient fault handling capabilities of the protocols.
The most prominent advantage of software verification over testing is a rigorous check of every possible software behavior. However, large state spaces of concurrent systems, due to non-deterministic ...scheduling, result in a slow automated verification process. Therefore, verification introduces a large delay between completion and deployment of concurrent software. This paper introduces a novel iterative approach to verification of concurrent programs that drastically reduces this delay. By restricting the execution of concurrent programs to a small set of admissible schedules, verification complexity and time is drastically reduced. Iteratively adding admissible schedules after their verification eventually restores non-deterministic scheduling. Thereby, our framework allows to find a sweet spot between a low verification delay and sufficient execution time performance. Our evaluation of a prototype implementation on well-known benchmark programs shows that after verifying only few schedules of the program, execution time overhead is competitive to existing deterministic multi-threading frameworks.
To aid the formal verification of fault-tolerant distributed protocols, we propose an approach that significantly reduces the costs of their model checking. These protocols often specify atomic, ...process-local events that consume a set of messages, change the state of a process, and send zero or more messages. We call such events quorum transitions and leverage them to optimize state exploration in two ways. First, we generate fewer states compared to models where quorum transitions are expressed by single-message transitions. Second, we refine transitions into a set of equivalent, finer-grained transitions that allow partial-order algorithms to achieve better reduction. We implement the MP-Basset model checker, which supports refined quorum transitions. We model check protocols representing core primitives of deployed reliable distributed systems, namely: Paxos consensus, regular storage, and Byzantine-tolerant multicast. We achieve up to 92% memory and 85% time reduction compared to model checking with standard unrefined single-message transitions.
Sclerotinia sclerotiorum is one of the most important pathogens of winter oilseed rape plants. It causes the white mould disease of rape, thus significantly reducing the yield. The aim of our ...research was to use a spring oilseed rape variety sown in autumn or an early-flowering variety of winter oilseed rape to predict the infection pressure of S. sclerotiorum in a given year. Field experiments were conducted in 2008–2012 at the experimental station of the Czech University of Life Sciences Prague at Červený Újezd, 20 km west of Prague. In the experiment, we used one variety of spring oilseed rape (Lužnice, LU) and one early-flowering variety of winter oilseed rape (Californium, CA). The methodology of the petal test involved isolating pathogenic fungi from fallen petals on a nutrient medium (potato dextrose agar) in Petri dishes. The first term of collection was the beginning of petal fall (BBCH 61) and the last term was the end of flowering (BBCH 69). The dishes with petals were visually analysed after 1 week. The results were compared with the actual occurrence of white mould of rape in the stand. The occurrence of white mould of rape was strongly influenced by the progress of weather conditions over the given year. Infected petals and stems with symptoms of white mould of rape were found to be moderately correlated (r = 0.80). Spread of white mould spores was mostly observed in two terms (BBCH 62 and BBCH 65). Statistically significant differences were not observed in the infection of petals of spring (LU) and winter (CA) oilseed rape. Spring oilseed rape (LU) and early-flowering varieties of winter oilseed rape (CA) can be used to determine the strength of infection pressure of S. sclerotiorum in the stand in a given year, thereby improving protection against white mould of rape.
•We used early-flowering varieties of oilseed rape to predict the infection pressure of Sclerotinia.•In the petal test, pathogenic fungi from fallen petals were isolated in Petri dishes.•The percentage of infected petals was compared with the real occurrence of white mould of rape.•Early-flowering varieties can provide information on the strength of infection pressure.
The complexity of distributed algorithms, such as state machine replication, motivates the use of formal methods to assist correctness verification. The design of the formal model of an algorithm ...directly affects the efficiency of the analysis. Therefore, it is desirable that this model does not add “unnecessary” complexity to the analysis. In this paper, we consider a general message-passing (MP) model of distributed algorithms and compare different ways of modeling the message traffic. We prove that the different MP models are equivalent with respect to the common properties of distributed algorithms. Therefore, one can select the model which is best suited for the applied verification technique.
We consider MP models which differ regarding whether (1) the event of message delivery can be interleaved with other events and (2) a computation event must consume all messages that have been delivered after the last computation event of the same process. For generalized MP distributed protocols and especially focusing on fault-tolerance, we show that our proposed model (without interleaved delivery events and with relaxed semantics of computation events) is significantly more efficient for explicit state model checking. For example, the model size of the Paxos algorithm is 1/13th that of existing equivalent MP models.
Production of medicinal plants is accompanied by many problems, out of which some are overcome. Problems in medicinal plant production, including the production of sage and lemon balm that cannot be ...avoided are pathogens, the presence of insects and weeds. During the summer of 2003 and 2004, the occurrence of animal pests and pathogens was investigated in the medicinal plants lemon balm (Mellisa officinalis) and garden sage (Salvia officinalis). The pathogens Alternaria alternata and Fusarium moniliforme and the insects Eupterix atropunctata and Empoasca pteridis (Homoptera, Cicadelidae) were identified as the cause of various damages to medicinal plants.
Pri uzgoju lekovitog bilja srecemo se sa razlicitim problemima, medju njima i sa pojavom korova, bolesti i stetocina. S ovim stetnim faktorima srecemo se i pri uzgoju melise i zalfije. Pojava bolesti i stetocina u usevu melise (Mellisa officinalis) i zalfije (Salvia officinalis) pracena je tokom leta 2003. i leta 2004. godine. Ustanovili smo pojavu sledecih patogena: Alternaria alternata i Fusarium spp. i sledece vrste insekata: Eupterix atropunctata i Empoasca pteridis (Homoptera, Cicadelidae), koje mogu ostecivati lekovito bilje i prouzrokovati snizenje kako kvantiteta tako i kvaliteta droge.
Fault-tolerant (FT) distributed protocols (such as group membership, consensus, etc.) represent fundamental building blocks for many practical systems, e.g., the Google File System. Not only does one ...desire rigor in the protocol design but especially in its verification given the complexity and fallibility of manual proofs. The application of model checking (MC) for protocol verification is attractive with its full automation and rich property language. However, being an exhaustive exploration method, its scalable use is very much constrained by the overall number of different system states. We observe that, although FT distributed protocols usually display a very high degree of symmetry which stems from permuting different processes, MC efforts targeting their automated verification often disregard this symmetry. Therefore, we propose to leverage the framework of symmetry reduction and improve on existing applications of it by specifying so called role-based symmetries. Our secondary contribution is to define a high-level description language called FTDP to ease the symmetry aware specification of FT distributed protocols. FTDP supports synchronous as well as asynchronous protocols, a variety of fault types, and the specification of safety and liveness properties. Specifications written in FTDP can directly be analyzed by tools supporting symmetry reduction. We demonstrate the benefit of our approach using the example of well-known and complex distributed FT protocols, specifically Paxos and the Byzantine Generals.
This paper presents efficient model checking of distributed software. Key to the achieved efficiency is a novel stateful model checking strategy that is based on the decomposition of states into a ...relevant and an auxiliary part. We formally show this strategy to be sound, complete, and terminating for general finite-state systems. As a case study, we implement the proposed strategy within Basset/MP-Basset, a model checker for message-passing Java programs. Our evaluation with actual deployed fault-tolerant message-passing protocols shows that the proposed stateful optimization is able to reduce model checking time and memory by up to 69% compared to the naive stateful search, and 39% compared to partial-order reduction.
PDF
