1,721,093 research outputs found
VIBE: Looking for Variability In amBiguous rEquirements
No full textVariability is a characteristic of a software project and describes the fact that a system can be configured in different ways, obtaining different products (variants) from a common code base, accordingly to the software product line paradigm. This paradigm can be conveniently applied in all phases of the software process, starting from the definition and analysis of the requirements. We observe that often requirements contain ambiguities which can reveal an unintentional and implicit source of variability, that has to be detected.To this end we define VIBE, a tool supported process to identify variability aspects in requirements documents. VIBE is defined on the basis of a study of the different sources of ambiguity in natural language requirements documents that are useful to recognize potential variability, and is character-ized by the use of a NLP tool customized to detect variability indicators. The tool to be used in VIBE is selected from a number of ambiguity detection tools, after a comparison of their customization features. The validation of VIBE is conducted using real-world requirements documents.(c) 2022 Elsevier Inc. All rights reserved
From generic requirements to variability
No full textThis paper describes a research activity aiming at extracting variability information from ambiguities and vagueness of generic requirement documents, written in Natural Language. The proposed activity continues a research stream focusing on techniques to extract variability information from requirement documents. Here, we study the introduction of a process able to distinguish structural from functional variability, both in the extracted variability model and in the derived lower-level requirements. The problem is stated with reference to an example, a solution proposal is sketched together with related research questions, and a validation path is envisaged
Formal Description and Validation for an Integrity Policy Supporting Multiple Levels of Criticality
No full textModel checking fault tolerant systems
No full textThis paper proposes a modelling approach suitable for formalizing fault tolerant systems, taking into account different fault scenarios. Verification of the properties of such systems is then performed using model checking. A general framework for the formal specification and verification of fault tolerant systems is defined starting from these principles, and experience with its application to two case studies is then presented
Two standards means problems: A case study on formal protocol descriptions
No full textEstelle and LOTOS Formal Description Techniques for protocol specifications are considered as a typical example of incompatibility problems which can arise when two standard are used in the same context.
The aim of this paper is to indicate the sources of possible problems and to show the effects of having incompatible specifications of the same system. A brief discussion follows on some techniques and methods to verify the compatibility between Estelle and LOTOS specifications
An Industrial Application for the JACK Environment
No full textJACK, Just Another Concurrency Kit, is a new environment integrating a set of formal verification tools, supported by a graphical interface offering facilities to use these tools separately or in combination. The environment proposes several functionalities for the design, analysis and verification of concurrent systems specified using formal methods. In this paper we outline an experience on formal specification of a real railway interlocking system using JACK. Then we verify, by using JACK'S checking capabilities, the correctness of the specification with respect to safety requirements. Our experience shows that the JACK environment can be applied successfully in the verification of real safety critical systems
Formal Validation of Fault-tolerance Mechanisms inside GUARDS
No full textIn this paper we report the experiments carried out during the specification and validation of the fault-tolerance mechanisms developed in the European project Generic Upgradable Architecture for Real-time Dependable Systems (GUARDS). These mechanisms are the components of an architecture developed for embedded safety-critical systems. The validation approach is based on model-checking techniques and exploits the verification methodology supported by the Just Another Concurrency Kit (JACK) environment. The properties that guarantee the desired behaviour of the mechanisms are specified as temporal logic formulae; the JACK model-checker is then used to verify that the behaviour of the mechanisms satisfy such properties also in the presence of faults
A Logic-Functional Approach to the Execution of CCS Specifications Modulo Behavioural Equivalences
No full textThis paper reports on a work that proposes a kernel for an execution environment for the operational semantics and the behavioural equivalences of CCS. The proposed execution environment distinguishes itself by being formal, by dealing with the behavioural equivalences as schemes of axioms, differently from other approaches based on automata, and by giving the possibility to define several strategies of verification in a modular and flexible way. The environment, obtained by techniques of logic-functional programming, treats basic CCS with bounded recursion. A particular strategy of verification is presented
- …
