An executable modeling and analyzing approach to C4ISR architecture

To analyze the behavioral model of the command,control,communication,computer,intelligence,surveillance,reconnaissance(C4ISR)architecture,we propose an executable modeling and analyzing approach to it.First,the meta concept model of the C4ISR architecture is introduced.According to the meta concept model,we construct the executable meta models of the C4ISR architecture by extending the meta models of fUML.Then,we define the concrete syntax and executable activity algebra(EAA)semantics for executable models.The semantics functions are introduced to translating the syntax description of executable models into the item of EAA.To support the execution of models,we propose the executable rules which are the structural operational semantics of EAA.Finally,an area air defense of the C4ISR system is used to illustrate the feasibility of the approach.

Modeling and Verifying Concurrent Programs with Finite Chu Spaces

Finite Chu spaces are proposed for the modeling and verification of concurrent programs.In order to model not only typical concurrent behaviors but also modern exception handling and synchronization mechanisms,we design an enriched process algebra of Chu spaces from a practical point of view.To illustrate the power of finite Chu spaces and the process algebra while abstracting away from language-specific details,an imaginary concurrent programming language（ICL） is designed.A denotational semantics of ICL is presented using finite Chu spaces and the enriched process algebra.The valuation functions are fairly straightforward since the carefully designed operators have done much of the job.The enriched process algebra is also used as the specification language for Chu spaces,with which process-algebraic properties can be specified.Verification algorithms are presented with their time complexities discussed.