A systematic approach to integrate common timed security rules within a TEFSM-based system specification

Context

Formal methods are very useful in the software industry and are becoming of paramount importance in practical engineering techniques. They involve the design and modeling of various system aspects expressed usually through different paradigms. These different formalisms make the verification of global developed systems more difficult.

Objective

In this paper, we propose to combine two modeling formalisms, in order to express both functional and security timed requirements of a system to obtain all the requirements expressed in a unique formalism.

Method

First, the system behavior is specified according to its functional requirements using Timed Extended Finite State Machine (TEFSM) formalism. Second, this model is augmented by applying a set of dedicated algorithms to integrate timed security requirements specified in Nomad language. This language is adapted to express security properties such as permissions, prohibitions and obligations with time considerations.

Results

The proposed algorithms produce a global TEFSM specification of the system that includes both its functional and security timed requirements.

Conclusion

It is concluded that it is possible to merge several requirement aspects described with different formalisms into a global specification that can be used for several purposes such as code generation, specification correctness proof, model checking or automatic test generation. In this paper, we applied our approach to a France Telecom Travel service to demonstrate its scalability and feasibility.     

Time to line crossing for lane departure avoidance: a theoretical study and an experimental setting

The main goal of this paper is to develop a distance to line crossing (DLC) based computation of time to line crossing (TLC). Different computation methods with increasing complexity are provided. A discussion develops the influence of assumptions generally assumed for approximation. A sensitivity analysis with respect to vehicle parameters and positioning is performed. For TLC computation, both straight and curved vehicle paths are considered. The road curvature being another important variable considered in the proposed computations, an observer for its estimation is then proposed. An evaluation over a digitalized test track is first performed. Real data are then collected through an experiment carried out in test tracks with the equipped prototype vehicle. Based on these real data, TLC is then computed with the theoretically proposed methods. The obtained results outlined the necessity to take into consideration vehicle dynamics to use the TLC as a lane departure indicator.     

Sensor fault tolerant control of nonlinear Takagi–Sugeno systems. Application to vehicle lateral dynamics

This paper presents a new scheme for sensor fault tolerant control for nonlinear systems based on the Takagi–Sugeno modeling. First, a structured residual generator aimed at detecting and isolating sensor faults is designed. A bank of observers controlled either by only one system output or a set of outputs is then implemented, leading to a set of state estimates. The parallel distributed compensation structure is adopted to design the fault tolerant controller. The novelty in this paper is that the estimated state used in the controller is a weighted state vector obtained from all the estimated states provided by the different observers. The weighting functions depend on the residual vector signals delivered by the residual generator. They are designed to avoid crisp switches in the control law. Indeed, the interesting feature of the proposed approach is to avoid the commonly used switching strategy. For each residual component, the greater its magnitude is, the less the weight affected to the corresponding state estimate is. Consequently, the controller only uses estimations computed on the basis of healthy measurements. The closed‐loop stability is studied with the Lyapunov theory, and the obtained conditions are expressed as a set of linear matrix inequalities. The proposed residual generation and fault tolerant controller are applied to a vehicle lateral dynamics affected by sensor faults. Copyright © 2015 John Wiley & Sons, Ltd.     

Modeling of dynamic vehicle–road interactions for safety-related road evaluation

Usually, road safety is assessed by following adequate highway geometric design standards and can be controlled later by measurement and expertise. Nevertheless, interactions between vehicle dynamics and road characteristics cannot be simultaneously analyzed for these two means of safety evaluation. In this study, an analytical method based on road/vehicle physical interactions applied to road diagnosis is proposed. Vehicle “point” and “bicycle” models are used in this first approach. French highway geometric design standards and a statistical method are presented and evaluated on a real curve case. The proposed numerical criterion, for the “bicycle” model, is then compared to these two classical methods for the considered road section. Its advantages are that it takes into account several combined parameters, that road defects are precisely localized and that it provides hierarchically classified solutions to the road managers. After this comparison step, further improvements should be focused on the modeling of successive curves and on the improvement of the informations given to the road manager.     

A SPIN-based approach for detecting vulnerabilities in C programs

An approach is presented for the detection of software vulnerabilities using the widely known SPIN model checker. Classes of vulnerabilities in C programs that can be detected using the presented approach are discussed. We present the results of experiments on detecting vulnerabilities in student-made software tools implementing array processing algorithms.     

A formal approach based on UML and B for the specification and development of database applications

This article describes a formal approach to specify and develop database applications. This approach consists of two complementary phases. In the first phase, B specifications are automatically generated from UML class, state and collaboration diagrams describing the data and the transactions of the system we are developing. In the second phase, these specifications are successively refined until they become close enough to a relational implementation. The tool supporting this approach is implemented as an extension of the Rational Rose tool to develop and visualize graphical (UML) and formal (B) notations in a single environment.     

A Model-Based Controller for Interactive Delayed Haptic Feedback Virtual Environments

This paper addresses the stability of time-delayed force-reflecting displays used in virtual reality interactive systems. A novel predictive-like approach is proposed. The developed solution is stable and robust. Neither time delay estimation nor time delay behavior's knowledge are required. The controller applies to constant or time-varying delays without any adaptation. In this research, efforts are devoted towards making results easy to implement in commercial haptic libraries and interface build-in controllers. Moreover, although this study focuses on virtual environments haptics, it can easily spread to force feedback teleoperators.