Search

In a tokamak, magnetic sensors are the primary diagnostics used to estimate the quantities controlled in feedback by the plasma current, position and shape controller. As a consequence, the number and position of the magnetic sensors has a large impact on the performance of the magnetic control system and on the tokamak configuration. In this paper, we consider the problem of choosing an optimal set of magnetic sensors for the ITER tokamak. As performance index we consider the capability of reconstructing the first plasma current density moments. Indeed a good reconstruction of these parameters guarantees also a good reconstruction of the parameters usually controlled by the magnetic control system (e.g. plasma-wall gaps, position of the current centroid, plasma current, etc.). The problem of choosing the best set of magnetic sensors is converted in a suitable convex optimization problem. Our approach allows us also to evaluate the level of redundancy in a given set of magnetic sensors and hence it gives information on how to behave in case of sensor faults. Numerical simulations are included in order to show the effectiveness of the approach.

When using formal methods, security protocols are usually modeled with a high level of abstraction. In particular, encryption is assumed to be perfect and cryptographic algorithms and their parameters are often abstracted away. This paper states a set of constraints under which, if an abstract protocol model is secure, then a refined model, which takes into account cryptographic algorithms and parameters, is implied to be secure too. The paper also indicates possible exploitations of this result.

Spi Calculus is an untyped high level modeling language for security protocols, used for formal protocols specification and verification. In this paper, a type system for the Spi Calculus and a translation function are formally defined, inorder to formalize the refinement of a Spi Calculus specification into a Java implementation. Since the generated Java implementation uses a custom Java library, formal conditions on the custom Java library are also stated, so that, if the library implementation code satisfies such conditions, then the generated Java implementation correctly simulates the Spi calculus specification.

Spi2Java is a tool that enables semi-automatic generation of cryptographic protocol implementations, starting from verified formal models. This paper shows how the last version of spi2Java has been enhanced in order to enable interoperability of the generated implementations. The new features that have been added to spi2Java are reported here. A case study on the SSH transport layer protocol, along with some experiments and measures on the generated code, is also provided. The case study shows, with facts, that reliable and interoperable implementations of standard security protocols can indeed be obtained by using a code generation tool like spi2Java.