Formal specification and refinement of a safe train control function

Motivated by the design and development challenges of the BART case study, an approach for developing and analyzing a formal model for reactive systems is presented. The approach makes use of a domain specific language for specifying control algorithms able to satisfy competing properties such as safety and optimality. The domain language, called SPC, offers several key abstractions such as the state, the profile, and the constraint to facilitate problem specification. Using a high-level program transformation system such as HATS being developed at the University of Nebraska at Omaha, specifications in this modelling language can be transformed to ML code. The resulting executable specification can be further refined by applying generic transformations to the abstractions provided by the domain language. Problem dependent transformations utilizing the domain specific knowledge and properties may also be applied. The result is a significantly more efficient implementation which can be used for simulation and gaining deeper insight into design decisions and various control policies. The correctness of transformations can be established using a rewrite-rule based induction theorem prover Rewrite Rule Laboratory developed at the University of New Mexico.

facilitating formal specification acquisition by using recursive functions on context-free languages

Although formal specification techniques are very useful in software development, the acquisition of formal specifications is a difficult task. This paper presents the formal specification language LFC, which is designed to facilitate the acquisition and validation of formal specifications. LFC uses context-free languages for syntactic aspect and relies on a new kind of recursive functions, i.e. recursive functions on context-free languages, for semantic aspect of specifications. Construction and validation of LFC specifications are machine-aided. The basic ideas behind LFC, the main aspects of LFC, and the use of LFC and illustrative examples are described.

an intuitive formal proof for deadline driven scheduler

United Nations University, Int. Inst. for Softw. Technol., China; Vietnam National University, Hanoi, Vietnam; Vietnam Academy of Science and Technology, Vietnam

Verification of EL2 electronic absorption effect on charge transfer in semi-insulating GaAs

The electronic absorption of EL2 centers has been clarified to be related to the electron acid hole photoionizations, and the transition from its ground state to metastable state, respectively. Under an illumination with a selected photon energy in the near infrared region, these three processes with different optical cross sections will show different kinetics against the illumination time. It has recently been shown that the photosensitivity (measured under 1.25 eV illumination) of the local vibrational mode absorption induced by some deep defect centers in SI-GaAs is a consequence of the electron and hole photoionizations of EL2. This paper directly measures the kinetics of the electronic transition associated with EL2 under 1.25 eV illumination, which implies the expected charge transfer among different charge states of the EL2 center. A calculation based on a simple rate equation model is in good agreement with the experimental results.

etl workflow analysis and verification using backwards constraint propagation

University of Twente; Centre for Telematics and Information Technology; Netherlands Organisation for Scientific Research; Jacquard; Capgemini

Experimental verification of therapeutic doses for the superficially-placed tumor radiotherapy with heavy ions at HIRFL

Up to now, clinical trials of heavy-ion radiotherapy for superficially placed tumors have been carried out for six times and over 60 selected patients have been treated with 80—100 MeV/u carbon ions supplied by the Heavy Ion Research Facility in Lanzhou (HIRFL) at the Institute of Modern Physics, Chinese Academy of Sciences since November, 2006. A passive irradiation system and a dose optimization method for radiotherapy with carbon-ion beams have been developed. Experimental verification of longitudinally ...