Refine Your Search

Search Results

Viewing 1 to 4 of 4
Technical Paper

Dissolution of the Gap between Safety Requirements Written in a Natural Language and Formal Notations

2016-04-05
2016-01-0133
Safety concepts are essential to conform to functional safety standard ISO 26262 for automotive products. Safety requirements, which are a part of safety concepts, shall be satisfied by products to avoid hazards by vehicles to maintain their safety. Incompleteness of safety requirements must be avoided in deriving parent requirements to its children. However, measure for checking is only reviewing when the safety requirements are described in a natural language. This measure for checking is not objective or stringent. We developed a specification technique written in formal notation that addresses some of the shortcomings of capturing safety requirements for verification purposes. Safety requirements in this notation are expressed in goal tree models, which originate from goal-oriented requirement engineering Knowledge Acquisition in autOmated Specification (KAOS). Each requirement is written with propositional logic as the node of a tree.
Technical Paper

Formal Verification Method for Safety Diagnosis Software

2015-04-14
2015-01-0279
Functions and sizes of electronic control and software systems in automotives are being increased to achieve better controllability and reduce fuel consumption. A higher safety level is also demanded, so functional-safety standards are increasingly being introduced to in-vehicle systems. In safety critical systems, failure must be diagnosed and a system transited to a safe state when hardware failure occurs. Therefore, the failure diagnosis part of the basic software that takes charge of signal inputs and outputs processing must be verified for high accountability and explanations to a third party. To diagnose failure, the hardware and software that originally operate independently need to cooperate in principle. Hardware and software cooperating systems are not straight-forward to verify, because the combinations of conditions are too numerous for testing.
Technical Paper

Application of Model Checking to Automotive Control Software with Slicing Technique

2013-04-08
2013-01-0436
To detect difficult-to-find defects in automotive control systems, we have proposed a modeling method with a program slicing technique. In this method, a verifier adjusts the boundaries of source code to be extracted on a variable dependence graph, in a kind of data flow. We have developed software tools for this method and achieved a 35% decrease in total verification time on model checking. This paper provides some consideration on effective cases of the method from verification practices. There are two types of malfunction causes: one is the timing of processes (race conditions), and the other is complex logics. Each type requires different elements in external environment models. Furthermore, we propose regression verification based on the modeling method above, to further reduce verification time on model checking. The paper outlines tool extensions needed to realize regression verification.
Journal Article

Membership Middleware for Dependable and Cost-Effective X-by-Wire Systems

2008-04-14
2008-01-0478
Balancing between dependability and cost-effectiveness is essential to promote X-by-Wire systems in the next decade. To achieve this goal, we have so far proposed a network centric architecture based on a concept of autonomous decentralized systems, where if one node fails, the remaining normal nodes autonomously execute a backup control to maintain the system's functionality, as well as a membership middleware indispensable to this architecture to ensure the consistency of the node status information among all nodes. In this work, we implemented membership middleware on a hardware and software platform equivalent to one assumed to be used in actual X-by-Wire systems. This paper describes the implementation details and performance evaluation result, and shows that membership middleware and a real-time critical application can coexist within one microcontroller.
X