Abstract
This paper proposes the use of available PMU measurements for establishing network observability State estimation is an important EMS application for providing real time, reliable and qualitative information on the system state. The observability analysis is the necessary function of the whole network state estimation. This paper addresses the incorporation of PMU measurements with the purpose of full network observability. The methodology is validated by the results on IEEE 14, 30 and 57 bus test system.

Abstract
This paper presents the Inter-Module Communication (IMC) protocol, a message-oriented protocol designed and implemented in the Underwater Systems and Technology Laboratory (LSTS) to build interconnected systems of vehicles, sensors and human operators that are able to pursue common goals cooperatively by exchanging real-time information about the environment and updated objectives. IMC abstracts hardware and communication heterogeniety by providing a shared set of messages that can be serialized and transferred over different means. The described protocol contrasts with other existing application level protocols by not imposing or assuming a specific software architecture for client applications. Native support can be automatically generated for different programming languages and/or computer architectures resulting in optimized code which can be used both for networked nodes and also for inter-process and inter-thread communication. The protocol has already been tested throughout various experiments led by LSTS where it has taken care of communications between vehicles, sensors and operator consoles. We are now developing the protocol in the direction of having multi-vehicle cooperation using live data from environmental sensors and mixed-initiative user interaction.

Abstract
A fabricated micro-mechanical sensor to assess the condition of automotive shock absorbers is presented. The monolithic sensor, measures the oil temperature, acceleration and internal pressure of the shock absorber. A dual mass accelerometer with optimized beam geometry is used for acceleration readout. In addition, a 23.1 mu m thickness square membrane and two buried resistors are used for pressure and temperature sensing respectively. The proposed miniaturized sensor can be effectively integrated with standard single- and dual-tube shock absorbers. The data acquired during normal vehicle operation can be continuously used to monitor the condition of the shock absorbers, allowing shock absorbers to be replaced before their degradation significantly reduce the comfort, performance and safety of the vehicle.

Abstract
Tool interoperability as a mean to achieve integration is among the main goals of the international Grand Challenge initiative. In the context of the Verifiable file system mini-challenge put forward by Rajeev Joshi and Gerard Holzmann, this paper focuses on the integration of different formal methods and tools in modelling and verifying an abstract file system inspired by the Intel Flash File System Core. We combine high-level manual specification and proofs with current state of the art mechanical verification tools into a tool-chain which involves Alloy, VDM++ and HOL. The use of (pointfree) relation modelling provides the glue which binds these tools together. © 2009 Springer-Verlag Berlin Heidelberg.

Abstract
This paper analyzes the dynamic performance of two cooperative robot manipulators. It is studied the implementation of fractional-order algorithms in the position/force control of two cooperating robotic manipulators holding an object. The simulations reveal that fractional algorithms lead to performances superior to classical integer-order controllers.

Abstract
The pointfree transform offers to the predicate calculus what the La-place transform offers to the differential/integral calculus: the possibility of changing the underlying mathematical space so as to enable agile algebraic calculation. This paper addresses the foundations of the transform and its application to a calculational approach to extended static checking (ESC) in the context of abstract modeling. In particular, a calculus is given whose rules help in breaking the complexity of the proof obligations involved in static checking arguments. The close connection between such calculus and that of weakest pre-conditions makes it possible to use the latter in ESC proof obligation discharge, where pointfree notation is again used, this time to calculate with invariant properties to be maintained. A connection with the "everything is a relation" lemma of Alloy is established, showing how close to each other the pointfree and Alloy notations are. The main advantage of this connection is that of complementing pen-and-paper pointfree calculations with model checking support wherever validating sizable abstract models.