Linux Driver Verification

h1. Formalizing Safety Rules 2

Before starting formalizing safety rules you need to create an account at this site. The name of this account should be sent to managers of the LDV project, e.g. via e-mail. Then somebody will add you to developers of the LDV project and you will be able to create and to update feature requests and bug reports "here":http://forge.ispras.ru/projects/ldv-rules/issues. 

Formalizing safety rules consists of following activities that can be fully or partially repeated several times.

h2. Understanding and informal description of the rule

Just one time per each rule you need to reserve a rule identifier by creating a feature request "here":http://forge.ispras.ru/projects/ldv-rules/issues. The rule identifier is a number. This number should be greater by one then the maximum of already reserved numbers. Note that you won''t be able to change the rule identifier. 

To understand the rule you need:

* To read available documentation of the relevant kernel core API.

* To explore source code of the Linux kernel. For instance, you may use http://lxr.linux.no or http://lxr.free-electrons.com.  

* To analyze verification results that you will obtained at one of the following steps.

* To discuss it with developers of the LDV project. 

"Here":http://linuxtesting.org/ldv/online?action=show_rule&rule_id=0032 you can find an example of a good description of a rule.