Distributed Hash Tables (DHTs) remain to this day a central component of modern peer-to-peer (P2P) systems, which rely on complex DHT protocols to scale to millions of nodes. The correct operation of DHTs is therefore essential for the proper functioning of these systems. For this reason, formal methods have been employed to model and verify a range of correctness properties of various DHT protocols. However, these verification efforts have focused on protocol-specific properties, such as topological invariants, instead of functional properties. This focus limits our understanding of the precise guarantees offered by each protocol. We propose a protocol-independent axiomatization of DHT properties using Allen Temporal Logic (ATL). To validate our axiomatization, we have implemented it in the Alloy analyser and used our implementation both to establish a number of DHT-derived properties and to generate a set of DHT execution traces that cover an exhaustive list of DHT corner case behaviours.
Software specifications often come in the form of contracts, detailing in particular pre- and postconditions of functions, libraries or modules. Research on contracts often centers around questions of contract inference or contract validation. In this paper, we study the less investigated aspect of quality of contracts. More specifically, we define the concept of redundancy for preconditions and propose three techniques with differing efficiency and effectiveness for detecting redundant preconditions. All three techniques are implemented within a software verification tool, and we present results of an experimental evaluation on a dataset of more than 60 C programs. The results confirm differences in precision and resource consumption of the techniques but also reveal unexpected outcomes about the completeness of the most precise, predicate analysis based technique.
Critical software systems need strong safety and security guarantees, since a bug can have very bad consequences. Thus, we need powerful verification techniques, such as formal methods, to assess such systems. Frama-C is an Open-Source platform for formal analysis of C code. It comes with ACSL, a specification language based on function contracts. Recently, a Frama-C plug-in has been developed for stating and verifying Typestates properties. These properties restrict possible operations on objects of a given datatype, depending on their current state. This plug-in instruments the original program with ACSL annotations, in order to use the standard Frama-C analyzers. We propose a formalization for this instrumentation, in order to prove its correctness. To this end, we rely on the Skel metalanguage, the Necrocoq tool, and the Coq proof assistant.
A relevant issue in managing a complex software system is the quantitative assessment of the fulfillment degree of its requirements, as it provides a sound basis for identifying suitable design time or runtime corrective actions. However, this quantitative assessment must cope with the uncertainty that could affect the requirements specification and the data used in the assessment process. We tackle this problem, assuming the system requirements are specified through a hierarchical goal model. For this case, we propose an approach rooted in the fuzzy set and fuzzy logic theory for the quantitative assessment of the fulfillment degree of the goals specified in the goal model, considering the different kinds of uncertainty that could be present. Our result enriches the methodological and practical toolset available for managing complex software systems in uncertain scenarios, complementing other approaches based on different formal frameworks like probability theory.
