Maritime freight is a sector of high importance in the field of international trade. During the last decades, maritime freight transportation has been growing progressively, nowa- days,  in order to transport large quantities of materials and save  great distances,  it is     the most used transport system.   The maritime freight transport involves  a large num-   ber of companies, which generates a greater number of jobs and acquires an additional importance for the economy and trade of the country. However, in order to maritime transportation to be in optimal conditions, it must be accompanied by a network of infrastructures and strategic points that allow different companies to carry out their func- tions. Nowadays, large quantities of goods are transported through the sea, this is why a regulatory framework is needed to control the various limitations and restrictions that must be imposed at sea. The organization in charge of this work is the so-called SOLAS (Safety of Life At Sea), which is part of the United  Nations  department.  This  organi- zation is responsible, as mentioned above, for safety at sea for ships and goods, it acts according to the current situation and responding to different disasters. As a result of certain accidents, whether navigation or breakage, the last law that has implemented is known  as  Verified  Gross  Mass (VGM). This thesis is divided into two parts, the first one analyses the importance of maritime transport for the countries of  Spain  and  Sweden. It  will  show  the  repercussion  it has on the country and its different connections to transport the goods through the country, as well as future trends to move these goods for each country as well. To conclude this part, a comparison will be made between both countries. Secondly, a study will be car- ried out on the effect of the law that was implemented dated back on 1 July 2016, the so-called Verified Gross Mass. A study is carried out in order to assess the challenges and opportunities generated by this law for the different stakeholders involved in maritime transport and how they have been acting in the countries of Spain and Sweden. Hence, fi- nal conclusions can be obtained regarding the conduct of each stakeholder in each country. Finally, the importance of road transport as the large transport system will be high- lighted in combination with the maritime transportation in both countries. On the other hand, regulatory changes will make a cooperation between stakeholders in order to reduce the  impact  in  their activity.

The focus of this dissertation is on developing novel methods and extending existing ones to improve the security and reliability of fixed-wing unmanned aircraft systems (UAS). Specifically, we focus on three strands of work: i) designing UAS controllers with performance guarantees using the robust control framework, ii) developing tools for detection and mitigation of physical-layer security threats in UAS, and iii) extending tools from compositional verification to design and verify complex systems such as UAS. Under the first category, we use the robust H-infinity control approach to design a linear parameter-varying (LPV) path-following controller for a fixed-wing UAS that enables the aircraft to follow any arbitrary planar curvature-bounded path under significant environmental disturbances. Three other typical path-following controllers, namely, a linear time-invariant H-infinity controller, a nonlinear rate-tracking controller, and a PID controller, are also designed. We study the relative merits and limitations of each approach and demonstrate through extensive simulations and flight tests that the LPV controller has the most consistent position tracking performance for a wide array of geometric paths. Next, convex synthesis conditions are developed for control of distributed systems with uncertain initial conditions, whereby independent norm constraints are placed on the disturbance input and the uncertain initial state. Using this approach, we design a distributed controller for a network of three fixed-wing UAS and demonstrate the improvement in the transient response of the network when switching between different trajectories. Pertaining to the second strand of this dissertation, we develop tools for detection and mitigation of security threats to the sensors and actuators of UAS. First, a probabilistic framework that employs tools from statistical analysis to detect sensor attacks on UAS is proposed. By incorporating knowledge about the physical system and using a Bayesian network, the proposed approach minimizes the false alarm rates, which is a major challenge for UAS that operate in dynamic and uncertain environments. Next, the security vulnerabilities of existing UAS actuators are identified and three different methods of differing complexity and effectiveness are proposed to detect and mitigate the security threats. While two of these methods involve developing algorithms and do not require any hardware modification, the third method entails hardware modifications to the actuators to make them resilient to malicious attacks. The three methods are compared in terms of different attributes such as computational demand and detection latency. As for the third strand of this dissertation, tools from formal methods such as compositional verification are used to design an unmanned multi-aircraft system that is deployed in a geofencing application, where the design objective is to guarantee a critical global system property. Verifying such a property for the multi-aircraft system using monolithic (system-level) verification techniques is a challenging task due to the complexity of the components and the interactions among them. To overcome these challenges, we design the components of the multi-aircraft system to have a modular architecture, thereby enabling the use of component-based reasoning to simplify the task of verifying the global system property. For component properties that can be formally verified, we employ results from Euclidean geometry and formal methods to prove those properties. For properties that are difficult to be formally verified, we rely on Monte Carlo simulations. We demonstrate how compositional reasoning is effective in reducing the use of simulations/tests needed in the verification process, thereby increasing the reliability of the unmanned multi-aircraft system. / Doctor of Philosophy / Given the safety-critical nature of many unmanned aircraft systems (UAS), it is crucial for stake holders to ensure that UAS when deployed behave as intended despite atmospheric disturbances, system uncertainties, and malicious adversaries. To this end, this dissertation deals with developing novel methods and extending existing ones to improve the security and reliability of fixed-wing UAS. Specifically, we focus on three key areas: i) designing UAS controllers with performance guarantees, ii) developing tools for detection and mitigation of security threats to sensors and actuators of UAS, and iii) extending tools from compositional verification to design and verify complex systems such as UAS. Pertaining to the first area, we design controllers for UAS that would enable the aircraft to follow any arbitrary planar curvature-bounded path under significant atmospheric disturbances. Four different controllers of differing complexity and effectiveness are designed, and their relative merits and limitations are demonstrated through extensive simulations and flight tests. Next, we develop control design tools to improve the transient response of multi-mission UAS networks. Using these tools, we design a controller for a network of three fixed-wing UAS and demonstrate the improvement in the transient response of the network when switching between different trajectories. As for the contributions in the second area, we develop tools for detection and mitigation of security threats to the sensors and actuators of UAS. First, we propose a framework for detecting sensor attacks on UAS. By judiciously using knowledge about the physical system and techniques from statistical analysis, the framework minimizes the false alarm rates, which is a major challenge in designing attack detection systems for UAS. Then, we focus on another important attack surface of the UAS, namely, the actuators. Here, we identify the security vulnerabilities of existing UAS actuators and propose three different methods to detect and mitigate the security threats. The three methods are compared in terms of different attributes such as computational demand, detection latency, need for hardware modifications, etc. In regard to the contributions in the third area, tools from compositional verification are used to design an unmanned multi-aircraft system that is tasked to track and compromise an aerial encroacher, wherein the multi-aircraft system is required to satisfy a global system property pertaining to collision avoidance and close tracking. A common approach to verifying global properties of systems is monolithic verification where the whole system is analyzed. However, such an approach becomes intractable for complex systems like the multi-aircraft system considered in this work. We overcome this difficulty by employing the compositional verification approach, whereby the problem of verifying the global system property is reduced to a problem of reasoning about the system’s components. That being said, even formally verifying some component properties can be a formidable task; in such cases, one has to rely on Monte Carlo simulations. By suitably designing the components of the multi-aircraft system to have a modular architecture, we show how one can perform focused component-level simulations rather than conduct simulations on the whole system, thereby limiting the use of simulations during the verification process and, as a result, increasing the reliability of the system.

An interesting alternative for today's high efficiency variable speed drives is the Permanent Magnet-Assisted Synchronous Reluctance Motor drive, which belongs to the family of brushless synchronous AC motor drives. Generally, the reluctance torque of this motor is significant compared to the Permanent Magnet electrical torque. The advantage of increased reluctance torque is the decreased need of expensive permanent magnet (PM) material, which makes this solution thus cheaper than the respective permanent magnet motor. Also due to its synchronous operation, sensorless rotational control is possible along with higher power factor and better efficiency compared to the induction motor (IM). Therefore, this thesis first deals with the implementation of a vector control strategy for speed control of the PMa-synRM motor that can be applied to a washing machine application. The machine is supplied by a current controlled voltage source PWM inverter to control the instantaneous stator currents which are decided by the reference speed. Secondly, the thesis focuses on the sensorless speed operation of the PMa-SynRM to take advantage of the lower costs as well as increased system reliability which otherwise is not possible using the delicate speed or position sensors. The concept involves estimation of the rotor speed and/or position. There are several speed estimation techniques proposed by researchers and among them the observer based technique is proven and commonly used in the industry. The only requirements of the observer system are a very fast signal processor, specialized and optimized to perform complex mathematical calculations. The feasibility and effectiveness of the control techniques are verified using the experimental results, implemented using the Texas Instruments TMS320F2812 eZDSP controller board and the overall motor drive system in the laboratory.

Programs have precise semantics, so we can use mathematical proof to establish their properties. These proofs are often too large to validate with the usual "social process" of mathematics, so instead we create and check them with theorem-proving software. This software must be advanced enough to make the proof process tractable, but this very sophistication casts doubt upon the whole enterprise: who verifies the verifier? We begin with a simple proof checker, Level 1, that only accepts proofs composed of the most primitive steps, like Instantiation and Cut. This program is so straightforward the ordinary, social process can establish its soundness and the consistency of the logical theory it implements (so we know theorems are "always true"). Next, we develop a series of increasingly capable proof checkers, Level 2, Level 3, etc. Each new proof checker accepts new kinds of proof steps which were not accepted in the previous levels. By taking advantage of these new proof steps, higher-level proofs can be written more concisely than lower-level proofs, and can take less time to construct and check. Our highest-level proof checker, Level 11, can be thought of as a simplified version of the ACL2 or NQTHM theorem provers. One contribution of this work is to show how such systems can be verified. To establish that the Level 11 proof checker can be trusted, we first use it, without trusting it, to prove the fidelity of every Level n to Level 1: whenever Level n accepts a proof of some phi, there exists a Level 1 proof of phi. We then mechanically translate the Level 11 proof for each Level n into a Level n - 1 proof---that is, we create a Level 1 proof of Level 2's fidelity, a Level 2 proof of Level 3's fidelity, and so on. This layering shows that each level can be trusted, and allows us to manage the sizes of these proofs. In this way, our system proves its own fidelity, and trusting Level 11 only requires us to trust Level 1. / text

The project revolves around logistics and its adoption to the new rules. Theobjective of this project is to focus on minimizing data tampering to the lowest level possible.To achieve the set goals in this project, Decision support system and simulation havebeen used. However, to get clear insight about how they can be implemented, a systematicliterature review (Case Study incl.) has been conducted, followed by interviews with personnelat Kakinada port to understand the real-time complications in the field. Then, a simulatedexperiment using real-time data from Kakinada port has been conducted to achieve the set goalsand improve the level of transparency on all sides i.e., shipper, port and terminal.

Interval arithmetic is a means to compute verified results. However, a naive use of interval arithmetic does not provide accurate enclosures of the exact results. Moreover, interval arithmetic computations can be time-consuming. We propose several accurate algorithms and efficient implementations in verified linear algebra using interval arithmetic. Two fundamental problems are addressed, namely the multiplication of interval matrices and the verification of a floating-point solution of a linear system. For the first problem, we propose two algorithms which offer new tradeoffs between speed and accuracy. For the second problem, which is the verification of the solution of a linear system, our main contributions are twofold. First, we introduce a relaxation technique, which reduces drastically the execution time of the algorithm. Second, we propose to use extended precision for few, well-chosen parts of the computations, to gain accuracy without losing much in term of execution time.

Made available in DSpace on 2015-03-03T15:47:45Z (GMT). No. of bitstreams: 1 ValerioGMJpdf.pdf: 1265506 bytes, checksum: f1fe3ef975bfeb2fce1dad3319a33f34 (MD5) Previous issue date: 2009-09-09 / This work shows a project method proposed to design and build software components from the software functional m del up to assembly code level in a rigorous fashion. This method is based on the B method, which was developed with support and interest of British Petroleum (BP). One goal of this methodology is to contribute to solve an important problem, known as The Verifying Compiler. Besides, this work describes a formal model of Z80 microcontroller and a real system of petroleum area. To achieve this goal, the formal model of Z80 was developed and documented, as it is one key component for the verification upto the assembly level. In order to improve the mentioned methodology, it was applied on a petroleum production test system, which is presented in this work. Part of this technique is performed manually. However, almost of these activities can be automated by a specific compiler. To build such compiler, the formal modelling of microcontroller and modelling of production test system should provide relevant knowledge and experiences to the design of a new compiler. In ummary, this work should improve the viability of one of the most stringent criteria for formal verification: speeding up the verification process, reducing design time and increasing the quality and reliability of the product of the final software. All these qualities are very important for systems that involve serious risks or in need of a high confidence, which is very common in the petroleum industry / Este trabalho apresenta um m?todo de projeto proposta para veri ca??o formal do modelo funcional do software at? o n?vel da linguagem assembly. Esse m?todo ? fundamentada no m?todo B, o qual foi desenvolvido com o apoio e interesse da multinacional do setor de petr?leo e g?s British Petroleum (BP). A evolu??o dessa metodologia tem como objetivo contribuir na resposta de um importante problema, que pertence aos grandes desa os da computa??o, conhecido como The Verifying Compiler . Nesse contexto, o presente trabalho descreve um modelo formal do microcontrolador Z80 e um sistema real da ?rea de petr?leo. O modelo formal do Z80 foi desenvolvido e documentado, por ser um pr?-requisito para a veri ca??o at? n?vel de assembly. A m de validar e desenvolver a metodologia citada, ela foi aplicada em um sistema de teste de produ??o de po?os de petr?leo, o qual ? apresentado neste trabalho. Atualmente, algumas atividades s?o realizadas manualmente. No entanto, uma parte signifi cativa dessas atividades pode ser automatizada atrav?s de um compilador espec?fi co. Para esse m, a modelagem formal do microcontrolador e a modelagem do sistema de teste de produ??o fornecem conhecimentos e experi?ncias importantes para o projeto de um novo compilador. Em suma, esse trabalho deve melhorar a viabilidade de um dos mais rigorosos crit?rios de veri ca??o formal: acelerando o processo de verifica??o, reduzindo o tempo de projeto e aumentando a qualidade e con fian?a do produto de software final. Todas essas qualidades s?o bastante relevantes para sistemas que envolvem s?rios riscos ou exigem alta confian?a, os quais s?o muito comuns na ind?stria do petr?leo

Les méthodes formelles ont atteint un degré de maturité conduisant à la conception de systèmes de preuves généralistes, permettant à la fois de vérifier la correction de systèmes logiciels complexes ou de formaliser des mathématiques avancées. Mais souvent, l'accent est mis davantage sur la facilité du raisonnement sur les programmes plutôt que sur leur exécution efficace. L'antagonisme entre ces deux aspects est particulièrement sensible pour les algorithmes de calcul formel, dont la correction repose habituellement sur des concepts mathématiques élaborés, mais dont l'efficacité pratique est une préoccupation importante. Cette thèse développe des approches à l'étude formelle et l'exécution efficace de programmes en théorie des types, et plus précisément dans l'assistant à la preuve \coq{}. Dans un premier temps, nous présentons un environnement d'exécution permettant de compiler en code natif de tels programmes tout en conservant la généralité et l'expressivité du formalisme. Puis, nous nous intéressons aux représentations de données et plus particulièrement au lien formellement vérifié et automatisé entre représentations adaptées aux preuves ou au calcul. Ensuite, nous mettons à profit ces techniques pour l'étude d'algorithmes en algèbre linéaire, comme le produit matriciel de Strassen, le procédé d'élimination de Gauss ou la mise en forme canonique de matrices, dont notamment la forme de Smith pour les matrices sur un anneau euclidien. Enfin, nous ouvrons le champ des applications à la formalisation et au calcul certifié des groupes d'homologie de complexes simpliciaux issus d'images numériques. / Formal methods have reached a degree of maturity leading to the design of general-purpose proof systems, enabling both to verify the correctness of complex software systems and to formalize advanced mathematics. However, the ease of reasoning on programs is often emphasized more than their efficient execution. The antagonism between these two aspects is particularly significant for computer algebra algorithms, whose correctness usually relies on elaborate mathematical concepts, but whose practical efficiency is an important matter of concern. This thesis develops approaches to the formal study and the efficient execution of programs in type theory, and more precisely in the proof assistant \coq{}. In a first part, we introduce a runtime environment enabling the native code compilation of such programs while retaining the generality and expressiveness of the formalism. Then, we focus on data representations and in particular on the formally verified and automatized link between proof-oriented and computation-oriented representations. Then, we take advantage of these techniques to study linear algebra algorithms, like Strassen's matrix product, Gaussian elimination or matrix canonical forms, including the Smith normal form for matrices over a Euclidean ring. Finally, we open the field of applications to the formalization and certified computation of homology groups of simplicial complexes arising from digital images.

L'arithmétique par intervalles permet de calculer et simultanément vérifier des résultats. Cependant, une application naïve de cette arithmétique conduit à un encadrement grossier des résultats. De plus, de tels calculs peuvent être lents.Nous proposons des algorithmes précis et des implémentations efficaces, utilisant l'arithmétique par intervalles, dans le domaine de l'algèbre linéaire. Deux problèmes sont abordés : la multiplication de matrices à coefficients intervalles et la résolution vérifiée de systèmes linéaires. Pour le premier problème, nous proposons deux algorithmes qui offrent de bons compromis entre vitesse et précision. Pour le second problème, nos principales contributions sont d'une part une technique de relaxation, qui réduit substantiellement le temps d'exécution de l'algorithme, et d'autre part l'utilisation d'une précision étendue en quelques portions bien choisies de l'algorithme, afin d'obtenir rapidement une grande précision. / Interval arithmetic is a means to compute verified results. However, a naive use of interval arithmetic does not provide accurate enclosures of the exact results. Moreover, interval arithmetic computations can be time-consuming. We propose several accurate algorithms and efficient implementations in verified linear algebra using interval arithmetic. Two fundamental problems are addressed, namely the multiplication of interval matrices and the verification of a floating-point solution of a linear system. For the first problem, we propose two algorithms which offer new tradeoffs between speed and accuracy. For the second problem, which is the verification of the solution of a linear system, our main contributions are twofold. First, we introduce a relaxation technique, which reduces drastically the execution time of the algorithm. Second, we propose to use extended precision for few, well-chosen parts of the computations, to gain accuracy without losing much in term of execution time.

The main subject and aim of this master thesis is the development and practical testing of a collaboration schema between Czech Encyclopedia of Sociology (Sociologická encyklopedie) and the Czech Wikipedia and its sociology-related content. The collaboration between these two information resources is based on the idea that the Encyclopedia of Sociology can serve as a quality resource for writing and editing Wikipedia and vice versa, Wikipedia can potentially increase Encyclopedia of Sociology's visibility and findability. The theoretical part of the thesis presents information about academic knowledge resources and open collaboration knowledge resources. Last but not least the theoretical part contains information about current practices of collaboration between Academia and Wikipedia. The research part of the thesis presents the development of the collaboration schema and its testing. Methods of semi-structured interviews and field experiment are used within this research. In the first part, one conducts interviews with Czech sociology experts and Wikipedians who are active in the field of sociology or related social sciences. The second part of the research then uses a field experiment to verify to some extent the information from the interviews and to induce reaction from the Wikipedian...