The engineering of industrial systems, particularly in safety-critical domains such as railways, demands rigorous verification and validation processes to ensure system dependability. Formal methods have emerged as powerful tools to complement traditional software engineering practices. In the railway sector, which increasingly relies on complex, distributed, and cyber-physical control systems, formal methods have demonstrated particular value for many decades now. In this article, we provide a retrospective overview of the application of formal methods and tools in the railway domain, with emphasis on two prominent verification approaches and one frequently verified railway system: modeling and validation with the B method and tools and formal verification of interlocking systems by model checking. We explore their role in the design and development of key railway systems, highlighting both academic research and industrial success stories, as witnessed by international projects and initiatives. We conclude with an outlook on the potential of integrating AI and formal methods to enhance the efficiency of next-generation railway systems.

Previous work has investigated the adequacy of LLMs to detect inconsistencies in requirements documents, but has also shown their limitations with real case studies. In this paper, we propose a hybrid approach, which exploits traditional clustering techniques to help LLMs focus on potential inconsistencies. The approach was evaluated using a large security requirements document from the RE Open Data Initiative, with injected inconsistencies. Results show that combining LLM-based detection with rule-based clustering enhances both precision and recall.

Technological advances in modern Train Control Systems (TCSs) promise to improve dependability of railway transportation in terms of safety, availability, and capacity, notably by employing novel distancing policies such as Moving Block (MB) signaling and Virtual Coupling (VC), fueled by advanced train localization methods such as satellite positioning. At the same time, these technological advances raise notable concerns about the effects that uncertainty in critical TCS parameters (such as train position and speed) may have on dependability-related attributes. Recently, various approaches have been proposed to characterize such effects through quantitative measures, leveraging formal stochastic modeling and evaluation of the TCS behavior. In this paper, we illustrate the results of a systematic review of the literature on quantitative evaluation of dependability-related attributes of TCSs under uncertainty on vital parameters. Specifically, we have finally selected 42 relevant papers, published between 2011 and 2023, that succeed in giving, through an empirical perspective and classification, a comprehensive view of current research and practice in quantitative dependability assessment of TCSs.

Modal Transition Systems (MTS) are a well-known formalism that extend Labelled Transition Systems (LTS) with the possibility of specifying necessary and permitted behaviour. Coherent MTS (CMTS) have been introduced to model Software Product Lines (SPL) based on a correspondence between the necessary and permitted modalities of MTS transitions and their associated actions, and the core and optional features of SPL. In this paper, we address open problems of the coherent fragment of MTS and introduce the notions of refinement and thorough refinement of CMTS. Most notably, we prove that refinement and thorough refinement coincide for CMTS, while it is known that this is not the case for MTS. We also define (thorough) equivalence and strong bisimilarity of both MTS and CMTS. We show their relations and, in particular, we prove that also strong bisimilarity and equivalence coincide for CMTS, whereas they do not for MTS. Finally, we extend our investigation to CMTS equipped with Constraints (MTSC), originally introduced to express alternative behaviour, and we prove that novel notions of refinement and strong thorough refinement coincide for MTSC, and so do their extensions to strong (thorough) equivalence and strong bisimilarity.

With the rapid advancement of tools based on Artificial Intelligence, it is interesting to assess their usefulness in requirements engineering. In early experiments, we have seen that ChatGPT can detect inconsistency defects in natural language (NL) requirements, that traditional NLP tools cannot identify or can identify with difficulties even after domain-focused training. This study is devoted to specifically measuring the performance of ChatGPT in finding inconsistency in requirements. Positive results in this respect could lead to the use of ChatGPT to complement existing requirements analysis tools to automatically detect this important quality criterion. For this purpose, we consider GPT-3.5, the Generative Pretrained Transformer language model developed by OpenAI. We evaluate its ability to detect inconsistency by comparing its predictions with those obtained from expert judgments by students with a proven knowledge of RE issues on a few example requirements documents.

Service contracts characterise the desired behavioural compliance of a composition of services. Compliance is typically defined by the fulfilment of all service requests through service offers, as dictated by a given Service-Level Agreement (SLA). Contract automata are a recently introduced formalism for specifying and composing service contracts. Based on the notion of synthesis of the most permissive controller from Supervisory Control Theory, a safe orchestration of contract automata can be computed that refines a composition into a compliant one. To model more fine-grained SLA and more adaptive service orchestrations, in this paper we endow contract automata with two orthogonal layers of variability: (i) at the structural level, constraints over service requests and offers define different configurations of a contract automaton, depending on which requests and offers are selected or discarded, and (ii) at the behavioural level, service requests of different levels of criticality can be declared, which induces the novel notion of semi-controllability. The synthesis of orchestrations is thus extended to respect both the structural and the behavioural variability constraints. Finally, we show how to efficiently compute the orchestration of all configurations from only a subset of these configurations. A prototypical tool supports the developed theory.

No abstract available.

The engineering of software product lines begins with the identification of the possible variation points. To this aim, natural language (NL) requirement documents can be used as a source from which variability-relevant information can be elicited. In this paper, we propose to identify variability issues as a subset of the ambiguity defects found in NL requirement documents. To validate the proposal, we single out ambiguities using an available NL analysis tool, QuARS, and we classify the ambiguities returned by the tool by distinguishing among false positives, real ambiguities, and variation points, by independent analysis and successive agreement phase. We consider three different sets of requirements and collect the data that come from the analysis performed.

Featured modal contract automata (FMCA) have been proposed as a suitable formalism for modelling contract-based dynamic service product lines. A contract is a behavioural description consisting of offers and necessary and permitted service requests with different levels of criticality, to be matched with corresponding offers of other FMCA. Each contract is equipped with a feature constraint, whose features are offers or requests, and characterises a valid product orchestration. A safe orchestration of a product fulfils all necessary and the maximum number of permitted requests, such that all enabled features are available and none of its disabled features is. The entire product line orchestration can be computed from a subset of valid product orchestrations, by exploiting their (partial) ordering. The open-source prototypical toolkit FMCAT supports the specification and orchestration of FMCA, and it interfaces with FeatureIDE for importing feature models and their valid products. In this experience report, we show how to model a Hotel service product line with FMCA and how to analyse it with FMCAT.

A product line perspective may help to understand the possible variants in interactions between the subsystems of a large, cyber-physical system. This observation is exemplified in this paper by proposing a feature model of the family of ERTMS/ETCS train control systems and their foreseen extensions. This model not only shows the different components that have to be installed when deploying the system at the different levels established by the ERTMS/ETCS standards, but it also helps to identify and discuss specific issues, such as the borders between onboard and wayside equipment, different manufacturers of the subsystems, interoperability among systems developed at different levels, backward compatibility of trains equipped with higher level equipment running on lines equipped with lower level equipment, and evolution towards future trends of railway signalling. The feature model forms the basis for formal modelling of the behaviour of the critical components of the system and for evaluating the overall cost, effectiveness and sustainability, for example by adding cost and performance attributes to the feature model.

Summary European Union (EU) projects are means of the European Commission for funding research activities. Such projects address challenging research objectives by involving both academic and industrial partners, from several countries. Information and communication technologies–related projects often undertake to deliver a software system prototype. In such a context, most of the typical issues of global requirements engineering may emerge. Partners can have different background and expertise, needs are not sharply defined, and communication is hampered by linguistic and cultural differences. If these issues are not carefully taken into account from the beginning, problems frequently emerge during project execution. This paper presents the experience of applying a customized elicitation and refinement approach in the context of the Learn PAd EU project, which involved about 50 people. The approach combines collaborative elicitation and wiki‐based refinement sessions to come to a set of consolidated requirements. Lessons learnt are discussed as a guidance for researchers dealing with analogous issues in similar contexts. Some of the major observations refer to the importance of initial face‐to‐face meetings when combined with asynchronous remote interactions; the role of moderators that have to encourage collaboration and foster a shared understanding; and the definition of guidelines to select wiki‐based platforms.

Model-based approaches are widely used for analysing systems belonging to a variety of domains, including the transportation sector. A critical issue with models is their validation, in order to justifiably put reliance on the analysis results they provide (including non functional indicators such as reliability, performance and energy consumption). Typically, cross-validation is performed, e.g. through exercising modelling by different formalisms/tools or through forms of experimental analysis. In this paper, we address validation of a case study from the railway domain via formal techniques, specifically with automata-based models. Validation of interaction aspects of Stochastic Activity Networks models of rail road switch heaters, developed for the purpose of evaluating energy consumption and reliability indicators, is performed through a tool based on contract automata, a recently introduced formalism for verifying properties of communication-based applications.

The requirements elicitation process often starts with an interview between a customer and a requirements analyst. During these interviews, ambiguities in the dialogic discourse may reveal the presence of tacit knowledge that needs to be made explicit. It is therefore important to understand the nature of ambiguities in interviews and to provide analysts with cognitive tools to identify and alleviate ambiguities. Ambiguities perceived by analysts are sometimes triggered by specific categories of terms used by the customer such as pronouns, quantifiers, and vague or under-specified terms. However, many of the ambiguities that arise in practice cannot be rooted in single terms. Rather, entire fragments of speech and their relation to the mental state of the analyst need to be considered.In this paper, we show that particular types of ambiguities can be characterised by means of argumentation theory. Argumentation is the study of how conclusions can be reached through logical reasoning. In an argumentation theory, statements are represented as arguments, and conflict relations among statements are represented as attacks. Based on a set of ambiguous fragments extracted from interviews, we define a model of the mental state of the analyst during an interview and translate it into an argumentation theory. Then, we show that many of the ambiguities can be characterized in terms of 'attacks' on arguments. The main novelty of this work is in addressing the problem of explaining fragment-level ambiguities in requirements elicitation interviews through the formal modeling of the analyst's mental model using argumentation theory. Our contribution provides a data-grounded, theoretical basis to have a more complete understanding of the ambiguity phenomenon, and lays the foundations to design intelligent computer-based agents that are able to automatically identify ambiguities.

In requirements elicitation interviews, ambiguities identified by analysts can help to disclose the tacit knowledge of customers. Indeed, ambiguities might reveal implicit or hard to express information that needs to be elicited. The perception of ambiguity might depend on the subject who is acting as analyst, and different analysts might identify different ambiguities in the same interview. Based on this intuition, we propose to investigate the difference between ambiguities explicitly revealed by an analyst during a requirements elicitation interview, and ambiguities annotated by a reviewer who listens to the interview recording, with the objective of defining a method for interview review. We performed an exploratory study in which two subjects listened to a set of customer-analyst interviews. Only in 26% of the cases the ambiguities revealed by the analysts matched with the ambiguities found by the reviewers. In 46% of the cases, ambiguities were found by the reviewers, and were not detected by the analysts. Based on these preliminary findings, we are currently performing a controlled experiment with students of two universities, which will be followed by a real-world case study with companies. This paper discusses the current results, together with our research plan.

This paper presents PURE (PUblic REquirements dataset), a dataset of 79 publicly available natural language requirements documents collected from the Web. The dataset includes 34,268 sentences and can be used for natural language processing tasks that are typical in requirements engineering, such as model synthesis, abstraction identification and document structure assessment. It can be further annotated to work as a benchmark for other tasks, such as ambiguity detection, requirements categorisation and identification of equivalent re-quirements. In the paper, we present the dataset and we compare its language with generic English texts, showing the peculiarities of the requirements jargon, made of a restricted vocabulary of domain-specific acronyms and words, and long sentences. We also present the common XML format to which we have manually ported a subset of the documents, with the goal of facilitating replication of NLP experiments.

Customer-analyst interviews are considered among the most effective means to perform requirements elicitation. However, during these interviews, ambiguity can hamper communication between customer and requirements analyst. Ambiguity is particularly dangerous in those cases in which the analyst misunderstands some linguistic expression of the customer, with-out being aware of the misunderstanding. On the other hand, if the analyst is able to detect ambiguous situations, this has been shown to help him/her in disclosing tacit knowledge. Indeed, the occurrence of an ambiguity might reveal the presence of unexpressed, system-relevant knowledge that needs to be elicited. Therefore, for the requirements elicitation interview to succeed, it is important for the analyst not to overlook ambiguities. To support the ambiguity-awareness of the requirements analyst, this paper aims to provide a set of cues that can be identified in the linguistic expressions of the customer, and that typically lead to ambiguity. To this end, we performed 34 customer-analyst interviews, and we isolated the speech fragments that caused the ambiguity. Based on the analysis of these fragments, and leveraging the previous literature on ambiguity in written requirements, we identified a set of cues that can be used by requirements analysts as a reference handbook to detect ambiguities.

Despite their significant advantages, formal methods are not widely used in industrial software development. Following the successful workshops we organized at ICSE 2103 in San Francisco, and ICSE 2014 in Hyderabad, we organize a third edition of the FormaliSE workshop with the main goal to promote the integration between the formal methods and the software engineering communities.

Interviews are the most common and effective means to perform requirements elicitation and support knowledge transfer between a customer and a requirements analyst. Ambiguity in communication is often perceived as a major obstacle for knowledge transfer, which could lead to unclear and incomplete requirements documents. In this paper, we analyse the role of ambiguity in requirements elicitation interviews. To this end, we have performed a set of customer-analyst interviews to observe how ambiguity occurs during requirements elicitation. From this direct experience, we have observed that ambiguity is a multi-dimensional cognitive phenomenon with a dominant pragmatic facet, and we have defined a phenomenological framework to describe the different types of ambiguity in interviews. We have also discovered that, rather than an obstacle, the occurrence of an ambiguity is often a resource for discovering tacit knowledge. Starting from this observation, we have envisioned the further steps needed in the research to exploit these findings.

Engineering a Collective Adaptive System (CAS) requires the support of a framework for quantitative modeling and analysis of the system. In order to jointly address variability and quantitative analysis, we apply the Product Lines paradigm, considered at the level of system engineering, to a case study of the European project QUANTICOL, by first defining a reference feature model and then adding feature attributes and global quantitative constraints, in the form of a Clafer attributed feature model. ClaferMOOVisualizer is subsequently used for quantitative analyses and multi-objective optimization of the resulting attributed feature model.

We show how the FMC model checker can successfully be used to model and analyze behavioural variability in Software Product Lines. FMC accepts parameterized specifications in a process-algebraic input language and allows the verification of properties of such models by means of efficient on-the-fly model checking. The properties can be expressed in a logic that allows to correlate the parameters of different actions within the same formula. We show how this feature can be used to tailor formulas to the verification of only a specific subset of products of a Software Product Line, thus allowing for scalable family-based analyses with FMC. We present a proof-of-concept that shows the application of FMC to an illustrative Featured Transition System from the literature.

A business subject who wishes to enter an established technological market is required to accurately analyse the features of the products of the different competitors. Such features are normally accessible through natural language (NL) brochures, or NL Web pages, which describe the products to potential customers. Building a feature model that hierarchically summarises the different features available in competing products can bring relevant benefits in market analysis. A company can easily visualise existing features, and reason about aspects that are not covered by the available solutions. However, designing a feature model starting from publicly available documents of existing products is a time consuming and error-prone task. In this paper, we present two tools, namely Commonality Mining Tool (CMT) and Feature Diagram Editor (FDE), which can jointly support the feature model definition process. CMT allows mining common and variant features from NL descriptions of existing products, by leveraging a natural language processing (NLP) approach based on contrastive analysis, which allows identifying domain-relevant terms from NL documents. FDE takes the commonalities and variabilities extracted by CMT, and renders them in a visual form. Moreover, FDE allows the graphical design and refinement of the final feature model, by means of an intuitive GUI.

Despite their significant advantages, formal methods are not widely used in industrial software development. FormaliSE is a workshop with the main goal to promote integration between the formal methods and the software engineering communities with the purpose to examine the link between the two more carefully than is done currently, and to better understand the reasons why this still is the case.

This paper presents a novel approach for pragmatic ambiguity detection in natural language (NL) requirements specifications defined for a specific application domain. Starting from a requirements specification, we use a Web-search engine to retrieve a set of documents focused on the same domain of the specification. From these domain-related documents, we extract different knowledge graphs, which are employed to analyse each requirement sentence looking for potential ambiguities. To this end, an algorithm has been developed that takes the concepts expressed in the sentence and searches for corresponding “concept paths” within each graph. The paths resulting from the traversal of each graph are compared and, if their overall similarity score is lower than a given threshold, the requirements specification sentence is considered ambiguous from the pragmatic point of view. A proof of concept is given throughout the paper to illustrate the soundness of the proposed strategy.

We demonstrate an experimental tool for the modeling and analysis of behavioral variability in product families.

We propose the Controlled Language for Software Product Lines CL4SPL with the twofold aim of ensuring simplicity of use for product line engineers and safe translations to executable languages amenable for automated verification. We show an implementation of CL4SPL in Maude, a well-known rewrite engine, thus allowing formal analyses over product families specified with CL4SPL. We illustrate our approach with a toy family of coffee machines.

We introduce a logical verification methodology for checking behavioral properties of service-oriented computing systems. Service properties are described by means of SocL, a branching-time temporal logic that we have specifically designed for expressing in an effective way distinctive aspects of services, such as, acceptance of a request, provision of a response, correlation among service requests and responses, etc. Our approach allows service properties to be expressed in such a way that they can be independent of service domains and specifications. We show an instantiation of our general methodology that uses the formal language COWS to conveniently specify services and the expressly developed software tool CMC to assist the user in the task of verifying SocL formulas over service specifications. We demonstrate the feasibility and effectiveness of our methodology by means of the specification and analysis of a case study in the automotive domain.

We present a research agenda on an emerging topic in software engineering, namely the synergy between Software Product Line Engineering (SPLE) and Service-Oriented Computing (SOC). Our proposal is to develop rigorous modelling techniques as well as analysis and verification support tools for assisting organisations to plan, optimise, and control the quality of 'software service' provision, both at design time and at run time. We foresee a flexible engineering methodology according to which 'software service line organisations' can develop novel classes of service-oriented applications that can easily be adapted to customer requirements as well as to changes in the context in which, and while, they execute. By superposing variability mechanisms on current languages for service engineering, based on policies and strategies defined by service providers, we envision the possibility of identifying variability points that can be triggered at run time to increase adaptability and optimise the (re)use of resources.

We illustrate how to manage variability in a single logical framework consisting of a Modal Transition System (MTS) and an associated set of formulae expressed in the branching-time temporal logic MHML interpreted in a deontic way over such MTSs. We discuss the commonalities and differences with the framework of Classen et al. based on Featured Transition Systems and Linear-time Temporal Logic.

We report on the successful application of academic experience with formal modelling and verification techniques to an automotive scenario from the service-oriented computing domain. The aim of this industrial case study is to verify a priori, thus before implementation, certain design issues. The specific scenario is a simplified version of one of possible new services for car drivers to be provided by the in-vehicle computers.

Requirements analysis is an important phase in a software project. Automatic evaluation of natural language (NL) requirements documents has been proposed as a means to improve the quality of the system under development. QuARS Express is an automatic analyzer of natural language (NL) requirements able to manage complex and structured requirement documents containing metadata, and to produce an analysis report rich of information that points out linguistic defects and indications about the writing style of NL requirements.

In this paper we propose a behavioural model, namely the generalized extended modal transition systems, as a basis for the formalization of different notions of variability usually present in product families definitions. In particular, a GEMTS is able to define a family of products by telling at any state of the system whether some (and how many) transitions are optional or mandatory for any derived products of the family. The proposed model is compared with previous proposals also based on labelled transition systems, showing its higher generality, but also pointing out weaknesses that still need to be addressed with more expressive models. Hints on the solution of such weaknesses are given by the use of constraints expressed as temporal logic formulae.

Composition of Web services is much studied to support business-to-business and enterprise application integration in e-commerce. Current Web service composition approaches range from practical languages aspiring to become standards (like BPEL, WS-CDL, OWL-S and WSMO) to theoretical models (like automata, Petri nets and process algebras). In this paper we compare these approaches w.r.t. a selected set of characteristics (like trust, security and performance) and we advocate the use of formal models, and their tool support, to increase one's confidence in web service compositions. This paper can assist web service composition designers and developers to deliver lasting solutions, in concordance with the technology's critical needs.

Requirements evolve during the software development process. Requirements specification evolution determines changes both in terms of level of details and style of representation and it brings the requirements from the initial statement of the customer needs towards more detailed documents able to drive the software design, construction and verification. Controlling the evolution of requirements, usually written in natural language, is very important for the success of the whole software project because every step in the evolutionary path of requirements can introduce undesired changes or lacks of information. This paper describes an approach based on the formal concepts analysis that allows a systematic and precise verification of the consistency among different stages of natural language requirements evolution.

In this paper we propose a behavioural model, namely the Extended Modal Labeled Transition Systems, as a basis for the formalization of the different notions of variability usually present in product families definitions. In particular, an EMLTS is able to define a family of products by telling at any state of the system whether transitions are optional or compulsory for the products of the family. Based on this model, verification that a product belongs to a family can be carried out by means of automatic tools.

We report on a fruitful combination of applying academic experience with formal modelling and verification techniques to an industrial case study. The goal of the case study was to investigate a priori, i.e. before implementation, the effects of adding a lightweight and easy-to-use publish/subscribe (event) notification service to thinkteam--an asynchronous and dispersed groupware system which was developed by think3. Researchers from the Formal Methods and Tools (FM&T) group of ISTI-CNR--with a longstanding experience in research on the development and application of formal methods, notations, and software tools for the specification, design, and verification of complex computer systems--therefore teamed up with think3--a global provider of integrated product development solutions that provides mechanical design and Product Data Management (PDM) software catering the product management needs of design processes in the manufacturing industry. The technical details of this joint research effort have been documented elsewhere, here we report on the lessons learned from this experience.

Nowadays common practice indicates that the requirement engineering (RE) process critically influences the success of the system development life cycle. Several commercial tools allow to classify, archive and manage requirements and then to print out reports and requirement documents. QuARS (Quality Analyzer for Requirements Specifications) is an automatic analyzer of such requirement documents, developed by ISTI-CNR, that can be adopted to evaluate the document quality by linguistic point of view. This paper presents how a requirement management tool, an automatic document generator, and QuARS can be integrated to define an RE automation support. The case study investigates and highlights the efficacy and the role of such proposed support in the Siemens C.N.X. development process.

The unified modelling language has been introduced as a notation for modelling and reasoning about large and complex systems, and their design, across a wide range of application domains. System modelling and analysis techniques, especially those based on formal methods, are more and more used for enhancing traditional system engineering techniques for improving system quality. In particular this holds for model-based formal test case derivation using formal conformance testing. The contribution of the present paper is to provide a solid mathematical basis for conformance testing and automatic test case generation for UML statecharts (UMLSCs). We propose a formal conformance-testing relation for input-enabled transition systems with transitions labelled by input/output-pairs (IOLTSs). IOLTSs provide a suitable semantic model for a behavioural subset of UMLSCs. We also provide an algorithm which, for a UMLSC specification and the alphabet of implementations, generates a test suite. The algorithm is proven exhaustive and sound w.r.t. the conformance relation.

This paper presents PLUTO, a simple and intuitive methodology to manage the testing process of product lines, described as Product Lines Use Cases (PLUCs). PLUCs are an extension of the well-known Cockburn's Use Cases, a notation based on natural language descriptions of requirements. The proposed test methodology is based on the Category Partition method, and can be used to derive a generic Test Specification for the product line, and a set of relevant test scenarios for a customer specific application.

This article presents a semantic-based environment for reasoning about the behavior of mobile systems. The verification environment, called HAL, exploits a novel automata-like model that allows finite-state verification of systems specified in the π-calculus. The HAL system is able to interface with several efficient toolkits (e.g. model-checkers) to determine whether or not certain properties hold for a given specification. We report experimental results on some case studies.

The Use Case formalism is an effective way of capturing both business process and functional system requirements in a very simple and easy-to-learn way. Use Cases may be modeled in a graphical way (e.g. using the UML notation), mainly serving as a table of content for Use Cases. System behavior can more effectively be specified by structured natural language (NL) sentences. The use of NL as a way to specify the behavior of a system is however a critical point, due to the inherent ambiguity originating from different interpretations of natural language descriptions. We discuss the use of methods, based on a linguistic approach, to analyze functional requirements expressed by means of textual (NL) Use Cases. The aim is to collect quality metrics and detect defects related to such inherent ambiguity. In a series of preliminary experiments, we applied a number of tools for quality evaluation of NL text (and, in particular, of NL requirements documents) to an industrial Use Cases document. The result of the analysis is a set of metrics that aim to measure the quality of the NL textual description of Use Cases. We also discuss the application of selected linguistic analysis techniques that are provided by some of the tools to semantic analysis of NL expressed Use Case.

Abstract This 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. Copyright © 2002 John Wiley & Sons, Ltd.

In this paper we present a verification framework to check properties of full CCS terms. These properties are expressed in an action-based logic, and the proof technique is model checking, based on the transition system corresponding to the CCS term. Our approach also allows some kinds of properties to be proved if the transition systems are infinite. Of course, in these cases we only have a semi-decision method. The idea is to use (a sequence of) finite-state transition systems which approximate the, possibly infinite, transition system corresponding to a term. To this end we define a particular notion of approximation, suitable in proving liveness and safety properties of the process terms. Then we show that the class of provable properties might also depend on the way chains of approximations are built and we provide a set of notions to compare and choose among different approximation chains.

This paper describes an experiment informal specification and validation performed in the context of an industrial joint project. The project involved an Italian company working in the field of railway engineering, Ansaldobreda Segnalamento Ferroviario, and the CNR Institutes IEI and CNUCE of Pisa, Within the project two formal models have been developed describing different aspects of a safety-critical system used in the management of medium-large railway networks. Validation of safety and liveness properties has been performed on both models. Safety properties have been checked primarily in presence of Byzantine faults as well as of silent faults embedded in the models themselves. Liveness properties have been more focused on a communication protocol used within the system. Properties have been specified by means of assertions or temporal logical formulae. We used PROMELA as specification language, while the verification was performed using the verification tool suite SPIN.

No abstract available.

Finding the solution of a dynamic programming problem m the form of polyadlc funcUonal equatmns is shown to be equivalent to searching a mmmaal cost path in an AND/OR graph with monotone cost functions The proof is given in an algebraic framework and is based on a commutaUvity result between solutton and mterpretauon of a symbohc system This approach Is simdar to the one used by some authors to prove the eqmvalence between the operaUonal and denotatmnal semantics of programming languages