Decision modeling is an essential part of the combat system effectiveness simulation (CoSES), which needs to cope with the cognitive quality, diversity, flexibility, and higher abstraction of decision making. In this paper, a multi-paradigm decision modeling framework is proposed to support decision modeling at three levels of abstraction based on domain-specific modeling (DSM). This framework designs a domain-specific modeling language (DSML) for decision modeling to raise the abstraction level of modeling, transforms the domain-specific models to formalism-based models to enable formal analysis and early verification and validation, and implements the semantics of the DSML based on a Python scripts framework which incorporates the decision model into the whole simulation system. The case study shows that the proposed approach incorporates domain expertise and facilitates domain modeler’s participation in CoSES to formulate the problem using DSML in the problem domain, and enables formal analysis and automatic implementation of the decision model in the solution domain.

Cyber physical systems (CPSs) can be found nowadays in various fields of activity. The increased interest for these systems as evidenced by the large number of applications led to complex research regarding the most suitable methods for design and development. A promising solution for specification, visualization, and documentation of CPSs uses the Object Management Group (OMG) unified modeling language (UML). UML models allow an intuitive approach for embedded systems design, helping end-users to specify the requirements. However, the UML models are represented in an informal language. Therefore, it is difficult to verify the correctness and completeness of a system design. The object constraint language (OCL) was defined to add constraints to UML, but it is deficient in strict notations of mathematics and logic that permits rigorous analysis and reasoning about the specifications. In this paper, we investigated how CPS applications modeled using UML deployment diagrams could be formally expressed and verified. We used Z language constructs and prototype verification system (PVS) as formal verification tools. Considering some relevant case studies presented in the literature, we investigated the opportunity of using this approach for validation of static properties in CPS UML models.

Yang and Chang (2009) proposed a three-party authenticated key exchange protocol for securing communications in mobile-commerce environments. Their protocol reduces computation and communication costs by employing elliptic curve cryptosystems. However, Tan (2010) pointed out that Yang and Chang (2009)’s protocol cannot withstand impersonation and parallel attacks, and further proposed an enhanced protocol to resist these attacks. This paper demonstrates that Tan (2010)’s approach still suffers from impersonation attacks, and presents an efficient and secure three-party authenticated key exchange protocol to overcome shown weaknesses.

Various solutions have been proposed to enable mobile users to access location-based services while preserving their location privacy. Some of these solutions are based on a centralized architecture with the participation of a trustworthy third party, whereas some other approaches are based on a mobile peer-to-peer (P2P) architecture. The former approaches suffer from the scalability problem when networks grow large, while the latter have to endure either low anonymization success rates or high communication overheads. To address these issues, this paper deals with an enhanced dual-active spatial cloaking algorithm (EDA) for preserving location privacy in mobile P2P networks. The proposed EDA allows mobile users to collect and actively disseminate their location information to other users. Moreover, to deal with the challenging characteristics of mobile P2P networks, e.g., constrained network resources and user mobility, EDA enables users (1) to perform a negotiation process to minimize the number of duplicate locations to be shared so as to significantly reduce the communication overhead among users, (2) to predict user locations based on the latest available information so as to eliminate the inaccuracy problem introduced by using some out-of-date locations, and (3) to use a latest-record-highest-priority (LRHP) strategy to reduce the probability of broadcasting fewer useful locations. Extensive simulations are conducted for a range of P2P network scenarios to evaluate the performance of EDA in comparison with the existing solutions. Experimental results demonstrate that the proposed EDA can improve the performance in terms of anonymity and service time with minimized communication overhead.

This paper focuses on the mechanism underlying the overall delay of a real-time video communication system from the time of capture at the encoder to the time of display at the decoder. A detailed analysis is presented to illustrate the delay problem. We then describe a statistically uniform intra-block refresh scheme for very low delay video communication. By scattering intra-blocks uniformly into continuous frames, the overall delay is significantly decreased, and object changes in the scene could be presented to the end user instantly. For comparison, the overall delay and the peak signal-to-noise ratio (PSNR) performance are tested. The experiment results show that an average of approximately 0.1 dB PSNR gain on average is obtained relative to random intra-macroblock refresh algorithm in H.264 JM, and the end-to-end delay performance is significantly improved.

The accuracy of microwave ranging is mainly limited by the frequency instability of the oscillator that generates the carrier phase signal. A dual transponder carrier ranging method is used to minimize the oscillator noise by combining the reference and the to-and-fro measurements. This ranging approach together with pseudo-noise ranging or other means can be used to measure the inter-satellite distance with a high precision. The pseudo-noise ranging system or other ranging systems help to solve the integer circles while the dual transponder ranging system guarantees the accurate fractional circle. The two satellites work in the master-slave mode. The range measurements are derived on the master satellite while the slave satellite just coherently transfers the received signal, so that the dual transponder ranging system does not need to rely on the time tagging system to synchronize the two satellites. This study first describes the dual transponder carrier ranging system and shows how the system removes most of the oscillator noise components effectively. Then, a detailed design scheme on the frequency planning of the ranging system is presented and the supporting analysis illustrates the feasibility of this system. Based on the design innovation, a laboratory demonstration system is assembled to verify the realizability of the dual transponder ranging system. The experimental results demonstrate that a high level of accuracy (about 30 μm under laboratory circumstance) can be achieved by the use of the proposed dual transponder carrier ranging system.