Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Applicability of Neural Networks for Driving Style Classification and Maneuver Detection
Full text linkManeuver and driving style detection are of ongoing interest for the extension of vehicle's functionalities. Existing machine learning approaches require extensive sensor data and demand for high computational power. For vehicle onboard implementation, poorly generalizing rule-based approaches are currently state of the art. Not being restricted to neither comprehensive environmental sensors like camera or radar, nor high computing power (both of what is today only present in upper class' vehicles), our approach allows for cross-vehicle use: In this work, the applicability of small artificial neural networks (ANN) as efficient detectors is tested using a prototypal vehicle implementation. During test drives, overtaking maneuvers have been detected 1.2 s prior to the competing rule-based approach in average, also greatly improving the detection performance. Regarding driving style recognition, ANN-based results are closer to targets and more patient at driving style transitions. A recognition rate of over 75 % is achieved
Formal Verification in the Loop to Enhance Verification of Safety-Critical Cyber-physical Systems
Full text linkFormal verification may play a central role in the development of safecontrollers, such as those found in electric drives or (semi-)autonomousvehicles, whose complexity arises from the coexistence ofmechanical and electrical subsystems with sophisticated electronic controllersthat must implement high-level control policies according to different drivingmodes, while optimizing several objectives, such as safety first and foremost,efficiency, and performance among others. Model-driven development resorts tosimulation to assess how well the various requirements and constraints aresatisfied, but there is a growing awareness that more rigorous methods areneeded to achieve the required levels of safety. This paper proposes aconceptual framework for the development of complex systems based on (i)higher-order logic specification, (ii) verification by theorem proving, and(iii) tight integration of verification with model-driven development andsimulation. This framework addresses both digital and analog systems, asillustrated with some examples in different fields including implantablebiomedical systems, autonomous vehicles, and electric valve actuation
Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Full text linkThere is a strong link between software quality and software reliability. By decreasing the probability of imperfection in the software, we can augment its reliability guarantees. At one extreme, software with one unknown bug is not reliable. At the other extreme, perfect software is fully reliable. Formal verification with SPARK has been used for years to get as close as possible to zero-defect software. We present the well-established processes surrounding the use of SPARK at Altran UK, as well as the deployment experiments performed at Thales to finetune the gradual insertion of formal verification techniques in existing processes. Experience of both long-term and new users helped us define adoption and usage guidelines for SPARK based on five levels of increasing assurance that map well with industrial needs in practice
Facilitating Automated Compliance Checking in the Safety-critical Context
No full textIn some safety-critical domains, the applicable safety standards prescribe a safety lifecycle and process-related requirements. Process plans in accordance with the prescribed requirements are essential pieces of evidence for compliance assessment with such standards. However, providing this evidence is time-consuming and prone-to-error since safety standards are large, natural language-based documents with hundreds of requirements. Besides, a company may have many safety-critical-related processes to be checked.In this paper, we propose a novel approach that combines process modeling and compliance checking capabilities to provide the analysis required to conclude whether a process model corresponds to the model with compliant states. Hitherto, our proposed methodology has been evaluated with academic examples that show the potential benefits of its use
Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
Full text linkSoftware-defined networks (SDN) offer a high degree of programmability for handling and forwarding packets. In particular, they allow network administrators to combine different security functions, such as firewalls, intrusion detection systems, and external services, into security chains designed to prevent or mitigate attacks against end user applications.These chains can benefit from formal techniques for their automated construction and verification. We propose in this paper a rule-based system for automating the composition and configuration of such chains for Android applications. Given the network characterization of an application and the set of permissions it requires, our rules construct an abstract representation of a custom security chain. This representation is then translated into a concrete implementation of the chain in pyretic, a domain-specific language for programming SDN controllers. We prove that the chains produced by our rules satisfy a number of correctness properties such as the absence of black holes or loops, and shadowing freedom, and that they are coherent with the underlying security policy
Rigorous Design of FDIR Systems with BIP
Full text linkThe correct design of autonomous systems is a challenge, due to the uncertainties arising at execution time. A special case of uncertainties are the faults and failures that break the system’s requirements. Dealing with such situations requires to design fault detection, isolation and recovery (FDIR) components. The aim of FDIR components is to detect when a fault has occurred and to apply a recovery strategy that brings the system into a mode where the requirements are satisfied. In this paper we describe an approach based on the Behavior, Interaction, Priority (BIP) tools for the rigorous design of FDIR components. This approach leverages the scalability of statistical model-checking tool BIP-SMC to check for requirement satisfaction, and the code generation feature of the BIP compiler. Moreover, the generated code is executable with the BIP engine(s) and easily integrated with the original system. The approach has been used in the H2020 ESROCOS and ERGO projects for the development of (autonomous) robotics control systems, which have been validated through field trials
Advances in Usability of Formal Methods for Code Verification with Frama-C
Full text linkIndustrial usage of code analysis tools based on semantic analysis, such as the Frama-C platform, poses several challenges, from the setup of analyses to the exploitation of their results. In this paper, we discuss two of these challenges. First, such analyses require detailed information about the code structure and the build process, which are often not documented, being part of the implicit build chain used by the developers. Unlike heuristics-based tools, which can deal with incomplete information, semantics-based tools require stubs or specifications for external library functions, compiler builtins, non-standard extensions, etc. Setting up a new analysis has a high cost, which precludes industrial users from trying such tools, since the return on investment is not clear in advance: the analysis may reveal itself of little use w.r.t. the invested time. Improving the usability of this first step is essential for the widespread adoption of formal methods in software development. A second aspect that is essential for successful analyses is understanding the data and navigating it. Visualizing data and rendering it in an interactive manner allows users to considerably speed up the process of refining the analysis results. We present some approaches to both of these issues, derived from experience with code bases given by industrial partners
Cross-Programming Language Taint Analysis for the IoT Ecosystem
Full text linkThe Internet of Things (IoT) is a key component for the next disruptive technologies. However, IoT merges together several diverse software layers: embedded, enterprise, and cloud programs interact with each other. In addition, security and privacy vulnerabilities of IoT software might be particularly dangerous due to the pervasiveness and physical nature of these systems. During the last decades, static analysis, and in particular taint analysis, has been widely applied to detect software vulnerabilities. Unfortunately, these analyses assume that software is entirely written in a single programming language, and they are not immediately suitable to detect IoT vulnerabilities where many different software components, written in different programming languages, interact. This paper discusses how to leverage existing static taint analyses to a cross-programming language scenario
Scalable Software Testing and Verification for Industrial-Scale Systems: The Challenges
Full text linkIn this position paper, we argue that more collaborative research is neededto increase the use of research-led verification and testing techniques in industrial-scale projects. We focus on the a) practical applicability and scalability of verification and testing techniques in industrial projects, and b) to autonomous systems. We identify the challenges involved and bring forward some initial suggestions