Search

Certifying safety-critical software and ensuring its safety requires checking the conformance between safety requirements and design. Increasingly, the development of safety-critical software relies on modeling, and the System Modeling Language (SysML) is now commonly used in many industry sectors. Inspecting safety conformance by comparing design models against safety requirements requires safety inspectors to browse through large models and is consequently time consuming and error-prone. To address this, we have devised a mechanism to establish traceability between (functional) safety requirements and SysML design models to extract design slices (model fragments) that filter out irrelevant details but keep enough context information for the slices to be easy to inspect and understand. In this article, we report on a controlled experiment assessing the impact of the traceability and slicing mechanism on inspectors' conformance decisions and effort. Results show a significant decrease in effort and an increase in decisions' correctness and level of certainty.

Coordinating a software project across distances is challenging. Even without geographical and time zone distances, other distances within a project can cause communication gaps. For example, organisational and cognitive distances between product owners and development-near roles such as developers and testers can lead to weak alignment of the software and the business requirements. Applying good software development practices, known to enhance alignment, can alleviate these challenges. We present a theoretical model called the Gap Model of how alignment practices affect different types of distances. This model has been inductively generated from empirical data. We also present an initial version of a theory based on this model that explains, at a general level, how practices affect communication within a project by impacting distances between people, activities and artefacts. The presented results provide a basis for further research and can be used by software organisations to improve on software practice.

An Introduction to Formal Methods is given within the scope of the book "Formal Methods for Industrial Critical Systems: A Survey of Applications Formal Methods for Industrial Critical Systems: A Survey of Applications"

Security is one of the main challenges of service oriented computing. Services need to be loosely coupled, easily ac- cessible and yet provide tight security guarantees enforced by cryptographic protocols. In this paper, we address how to automatically synthesize an orchestrator process able to guarantee the secure composition of electronic services, sup- porting different communication and cryptographic proto- cols. We present a theoretical model based on process alge- bra, partial model checking and logical satisfiability, plus an automated tool implementing the proposed theory.

The EU Future and Emerging Technologies (FET) Project Connect aims at dropping the heterogeneity barriers that prevent the eternality of networking systems through a revo- lutionary approach: to synthesise on-the- y the Connectors via which networked systems communicate. The Connect approach, however, comes at risk from the standpoint of de- pendability, stressing the need for methods and tools that ensure resilience to faults, errors and malicious attacks of the dynamically Connected system. We are investigat- ing a comprehensive approach, which combines dependabil- ity analysis, security enforcement and trust assessment, and is centred around a lightweight adaptive monitoring frame- work. In this project paper, we overview the research that we are undertaking towards this objective and propose a uni- fying work ow process that encompasses all the Connect dependability/security/trust concepts and models.

This paper reports on the Simulink/Stateflow based development of the on-board equipment of the Metro Rio Automatic Train Protection system. Particular focus is given to the strategies followed to address formal weaknesses and certification issues of the adopted tool-suite. On the development side, constraints on the Simulink/Stateflow semantics have been introduced and design practices have been adopted to gradually achieve a formal model of the system. On the verification side, a two-phase approach based on model based testing and abstract interpretation has been followed to enforce functional correctness and runtime error freedom. Quantitative results are presented to assess the overall strategy: the effort required by the design activities is balanced by the effectiveness of the verification tasks enabled by model based development and automatic code generation.

The paper introduces a general approach to the construction of a Quality Model for Web Sites. The process for constructing such a newly conceived model is presented and discussed, and examples of its application are shown.

The railway and metro signaling industries are currently investigating strategies for the introduction of formal model based development within their development processes. Among the various platforms supporting this technology, the Simulink/Stateflow tool-suite has been adopted in various safety-critical domains for modeling and code generation of controlsystems. Despite their flexibility and ease of use, introduction of these tools for developing dependable software, and in particular signaling applications, has been often hampered by the lack of a rigorous formal semantic sand by the absence of a certified code generator. This paper reports on the Simulink/Stateflow based development of the on-board equipment of the Metro Rio Automatic Train Protection system, describing the design strategy and the approach followed in addressing weaknesses and certification issues related to the adopted tool-suite.

We describe an approach to the analysis of protocols for wireless sensor networks in scenarios with mobile nodes and dynamic link quality. The approach is based on the theorem proving system PVS and can be used for formal specification, automated simulation and verification of the behaviour of the protocol. In order to demonstrate the applicability of the approach, we analyse the reverse path forwarding algorithm, which is the basic technique used for diffusion protocols for wireless sensor networks.

Web applications are widely adopted and their correct functioning is mission critical for many businesses. At the same time, Web applications tend to be error prone and implementation vulnerabilities are readily and commonly exploited by attackers. The design of countermeasures that detect or prevent such vulnerabilities or protect against their exploitation is an important research challenge for the fields of software engineering and security engineering. In this paper, we focus on one specific type of implementation vulnerability, namely, broken dependencies on session data. This vulnerability can lead to a variety of erroneous behavior at runtime and can easily be triggered by a malicious user by applying attack techniques such as forceful browsing. This paper shows how to guarantee the absence of runtime errors due to broken dependencies on session data in Web applications. The proposed solution combines development-time program annotation, static verification, and runtime checking to provably protect against broken data dependencies. We have developed a prototype implementation of our approach, building on the JML annotation language and the existing static verification tool ESC/Java2, and we successfully applied our approach to a representative J2EE-based e-commerce application. We show that the annotation overhead is very small, that the performance of the fully automatic static verification is acceptable, and that the performance overhead of the runtime checking is limited. ispartof: IEEE transactions on software engineering vol:34 issue:1 pages:50-64 status: published

Dynamic error processing approaches are an important mechanism to increase the reliability in a multiprocessor system, while making efficient use of the available resources. To this end, dynamic error processing must be integrated with a fault treatment approach aiming at optimising resource utilisation. In this paper we propose a diagnosis approach that, accounting for transient faults, tries to remove units very cautiously and to balance between two conflicting requirements. The first is to avoid the removal of units that have experienced transient faults and can be still useful for the system and the other is to avoid to keep failed units whose usage may lead to a premature failure of the system. The proposed fault treatment approach is integrated with a mechanism for dynamic error processing in a complete fault tolerance strategy. Reliability analyses based on the Markov approach and an efficiency evaluation performed by simulation are carried out.

Several techniques for specification exist to capture certain aspects of user behaviour, with the goal of reasoning about the usability of the system and other human-factors related issues. One such approach is to encode a set of assumptions about user behaviour in a user model. A difficulty with this approach is that human behaviour is inherently nondeterministic; humans make errors, perform unexpected actions, and, taken individually, both the occurrence of errors and response times can be unpredictable. Such factors, however can be expected to follow probability distributions, and so an interesting possibility is to apply stochasticor probabilistictec hniques that allow the modelling of uncertainty in user models. Recently, a number of process algebra based approaches to specifying stochastic systems have been proposed and in this paper we examine the possibility of applying these stochastic modelling techniques to reasoning about performance aspects of interactive systems.

Using cognitive architectures to analyse the usability of human-computer interfaces is an extensively investigated strategy. A particularly powerful way to perform such analysis is through syndetic modelling, where both the interface and the chosen cognitive model are described in the same specification framework; allowing the combined behaviour of the two to be analysed. This paper proposes LOTOS as a syndetic modelling language. We highlight four reasons why syndetic modelling is so difficult and show how the LOTOS notation addresses each of these four reasons.

This paper describes an experience in formal specification and fault tolerant behavior validation of a railway critical system. The work, performed in the context of a real industrial project, had the following main targets: (a) to validate specific safety properties in the presence of byzantine system components or of some hardware temporary faults; (b) to design a formal model of a critical railway system at a right level of abstraction so that could be possible to verify certain safety properties and at the same time to use the model to simulate the system. For the model specification we used the Promela language, while the verification was performed using the Spin model checker. Safety properties were specified by means of both assertions and temporal logic formulae. To make the problem of validation tractable in the Spin environment, we used ad hoca abstraction techniques.

Many of the reported experiences in the industrial use of formal methods concern the development of products or product families, where the utility of the method is linked to direct savings in development costs or improved assurance of quality. However, one other area in which formal description techniques make a valuable contribution is in the development and documentation of International Standards, where the cost of using formal methods can be paid off both through increased quality of products that implement a given standard, and through the improved inter-operability of different implementations that comes from having a precise definition of the expected behaviour of a conforming implementation. Standards development, however, has some significant differences from product development, and comes with specific needs and constraints that affect the use of formal description techniques. This paper describes the role that formal methods played in the development of a new standard for distributed multimedia presentation. It describes a number of issues that arose from this experience, and which have longer term importance for formal methods in standards, particularly given the changes that are taking place in the way that standards are developed.

JACK, 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. © 1997 Elsevier Science Inc.

The GEDBLOG system allows applications which manipulate graphic objects to be developed following a declarative definitional style. GEDBLOG supports the consistent design and prototyping of graphic applications through an incremental development and makes it possible to guarantee automatically that the application meets its specifications. Typical GEDBLOG applications have graphics as their characterizing element and can be found, for example, in the CAD/CAM, visual languages or graphical interface areas. The system is obtained by integrating a graphical data language in an existing logic database management system, EDBLOG, so that graphic and non-graphic information is handled in a uniform declarative way. © 1994 Academic Press, Inc.

This paper shows how formal modelling can be used in the design of a dynamic gesture language defined by sequences of poses. It discusses two models at different levels of abstraction dealing with important usability issues of the language such as ambiguity and overlap in the recognition of gestures. An approach to make the language more resilient to intermediate poses is evaluated based on a timed extension of the model. A tool providing model checking for hybrid automata is used to perform systematic and automatic analysis.

An abstract is not available.