Semantic theories of programs with nested interrupts

In the design of dependable software for embed- ded and real-time operating systems, time analysis is a cru- cial but extremely difficult issue, the challenge of which is exacerbated due to the randomness and nondeterminism of interrupt handling behaviors. Thus research into a theory that integrates interrupt behaviors and time analysis seems to be important and challenging. In this paper, we present a pro- gramming language to describe programs with interrupts that is comprised of two essential parts： main program and inter- rupt handling programs. We also explore a timed operational semantics and a denotational semantics to specify the mean- ings of our language. Furthermore, a strategy of deriving de- notational semantics from the timed operational semantics is provided to demonstrate the soundness of our operational se- mantics by showing the consistency between the derived de- notational semantics and the original denotational semantics.

A novel requirement analysis approach for periodic control systems

Periodic control systems （PCSs） are widely used in real-time embedded system domain. However, traditional manual requirement analysis assumes the expert knowledge, which is laborious and error-prone. This paper proposes a novel requirement analysis approach, which supports the automated validation of the informal requirement specifi- cations. Based on the normalized initial requirement docu- ments, our approach can construct an intermediate SPARDL model with both formal syntax and semantics. To check the overall system behaviors, our approach can transform the SPARDL models into executable code for simulation. The derived prototype simulator from SPARDL models enables the testing-based system behavior validation. Moreover, our approach enables the analysis of the dataflow relations in SPARDL models. By revealing input/output and affecting re- lations, our dataflow analysis techniques can help software engineers to figure out the potential data dependencies be- tween SPARDL modules. This is very useful for the module reuse when a new version of the system is developed. A study of our approach using an industry design demonstrates the practicality and effectiveness of our approach.

AADL+: a simulation-based methodology for cyber-physical systems

AADL (architecture analysis and design language) concentrates on the modeling and analysis of application system architectures.It is quite popular for its simple syntax,powerful functionality and extensibility and has been widely applied in embedded systems for its advantage.However,it is not enough for AADL to model cyber-physical systems (CPS) mainly because it cannot be used to model the continuous dynamic behaviors.This paper proposes an approach to construct a new sublanguage of AADL called AADL+,to facilitate the modeling of not only the discrete and continuous behavior of CPS,but also interaction between cyber components and physical components.The syntax and semantics of the sublanguage are provided to describe the behaviors of the systems.What's more,we develop a plug-in to OSATE (open-source AADL tool environment) for the modeling of CPS.And the plug-in supports syntax checking and simulation of the system model through linking with modelica.Finally,the AADL+ annex is successfully applied to model a lunar rover control system.

Hybrid MARTE statecharts

The specification of modeling and analysis of real-time and embedded systems （MARTE） is an extension of the unified modeling language （UML） in the domain of real-time and embedded systems. Even though MARTE time model offers a support to describe both discrete and dense clocks, the biggest effort has been put so far on the specifi- cation and analysis of discrete MARTE models. To address hybrid real-time and embedded systems, we propose to ex- tend statecharts using both MARTE and the theory of hybrid automata. We call this extension hybrid MARTE statecharts. It provides an improvement over the hybrid automata in that： the logical time variables and the chronometric time vari- ables are unified. The formal syntax and semantics of hybrid MARTE statecharts are given based on labeled transition sys- tems and live transition systems. As a case study, we model the behavior of a train control system with hybrid MARTE statecharts to demonstrate the benefit.