Formal specifications are mathematically based techniques with which a system can be analyzed, and its functionalities be described. Case studies have shown that using formal specifications can help reduce bugs and other inconsistencies when implementing a complex system; they are more likely found during the software design phase rather than later. During the process of porting code, testing has been used to verify that the port has the same functionalities as the original. However, testing alone has been deemed necessary but not sufficient to accomplish this. This thesis questions if formal specifications could be used during the process of porting code to create an accurate model of the system, and thereby provide higher degrees of certainty that the final product conforms to the original. A step-by-step methodology is presented to answer this question. The methodology ascertains the behavior of a port target through testing and a formal specification model based on these tests is created. This model is then used to create the port. The result indicates that the methodology used has some potential since it provided a high level of certainty that the ported code adhered to the original. Since the methodology puts a high emphasis on the specification and has several layers of verification, it is likely that it is suitable for projects with several modules and interdependencies. When using it for porting a trivial or non-complex system, the overhead of the methodology may prove high in comparison to the value gained. It was also found that one must take into consideration the implicit functionalities a language provides. Strict reliance on a model could thereby lead to a less flexible process where creativity and consideration of the specifics of the target language may have produced a different result. / Formella specifikationer är matematiska tekniker med vilka ett system kan analyseras och dess funktioner beskrivas. Fallstudier har visat att användning av formella specifikationer vid mjukvaruutveckling kan bidra till att reducera antalet fel och därmed minska omkostnaderna. Vid portering av kod har tester använts för att verifiera att porteringen har samma funktionaliteter som originalet. Tester anses dock vara otillräckliga - om än nödvändiga - för att fullständigt beskriva ett system. Denna avhandling ställer frågan om formella specifikationer kan användas i en porteringsprocess och därmed ge en högre grad av tillförlitlighet i att porteringen överensstämmer med originalet. En steg-för-steg-metodik presenteras för att besvara denna fråga. Metodiken använder sig av tester för att beskriva det system som skall porteras och en modell baserad på formella specifikationer skapas genom dessa tester. Denna modell används därefter för att skapa porteringen. Resultatet indikerar att metoden har viss potential eftersom den upplevdes öka förståelsen för referensarbetet och därmed också tryggheten i att den portade koden överensstämde med originalet. Eftersom metodiken lägger stor vikt vid specifikationen och består av flera lager av verifiering är det troligt att den är mer lämplig för system som består av flertalet moduler med inbördes beroende. Vid användning för att portera ett trivialt system kan metodens om-kostnader visa sig vara för höga i förhållande till det värde som erhålls. Det visade sig även att en porteringsprocess måste ta hänsyn till de implicita funktioner ett språk tillhandahåller. En strikt anpassning till en modell kan därmed leda till en mindre flexibel process och därmed leda till ett icke tillfredsställande resultat, där kreativitet och hänsyn till målspråket skulle kunna ha gett ett annat.

Une plateforme de conception est une solution totale qui permet à une équipe de conception de développer un système sur puce. Une telle plateforme se compose d'un ensemble de bibliothèques et de circuits réutilisables (IPs), d'outils de CAO et de kits de conception en conformité avec les flots de conception et les méthodologies supportés. Les spécifications de ce type de plateforme offrent un large éventail d'informations, depuis des paramètres de technologie, jusqu'aux informations sur les outils. En outre, les développeurs de bibliothèque/IP ont des difficultés à obtenir les données nécessaires à partir ces spécifications en raison de leur informalité et complexité. Dans cette thèse, nous proposons des méthodologies, des flots et des outils pour formaliser les spécifications d'une plateforme de conception et les traiter. Cette description proposée vise à être utilisée comme une référence pour générer et valider les bibliothèques et les IPs. Nous proposons un langage de spécification basé sur XML (nommé LDSpecX). De plus, nous présentons une méthode basée sur des références pour créer une spécification fiable en LDSpecX et des mots-clés basés sur des tâches pour en extraire les données efficacement. A l'aide des solutions proposées, nous développons une plateforme de spécification. Nous développons une bibliothèque de cellules standard en utilisant cette plateforme de spécification. Nous montrons ainsi que notre approche permet de créer une spécification complète et cohérente avec une réduction considérable du temps. Cette proposition comble également l'écart entre les spécifications et le système automatique existant pour le développement rapide de bibliothèques/IPs. / A design platform (DP) is a total solution to build a System-On-Chip (SOC). DP consists of a set of libraries/IPs, CAD tools and design kits in conformity with the supported design flows and methodologies. The DP specifications provide a wide range of information from technology parameters like Process-Voltage-Temperature (PVT) corners to CAD tools’ information for library/IP development. However, the library/IP developers have difficulties in obtaining the desired data from the existing specifications due to their informality and complexity. In this thesis, we propose methodologies, flows and tools to formalize the DP specifications for their unification and to deal with it. The proposed description is targeting to be used as a reference to generate and validate libraries (standard cells, I/O, memory) as well as complex IPs (PLL, Serdes, etc.). First, we build a suitable data model to represent all required information for library/IP development and then propose a specification language named Library Development Specification based on XML (LDSpecX). Furthermore, we introduce a reference-based method to create a reliable specification in LDSpecX and task-based keywords to efficiently extract data from it. On the basis of the proposed solutions, we develop a specification platform. Experimentally, we develop a standard cell library from the specification creation to library validation by using the specification platform. We show that our approach enables to create a complete and consistent specification with a considerable reduction in time. It also bridges the gap between the specification and current automatic system for rapid library/IP development.

La simulation multi-disciplinaire et multi-physique représente un enjeu scientifique et industriel majeur. La simulation a été essentiellement traitée par les physiciens (mécanique, électromagnétique, ...) comme un problème numérique sur des cas d'étude très précis mais n'a jamais été abordée d'un point de vue système. La problématique générale posée par la simulation de systèmes complexes inclut la composition des modèles, l'optimisation multi-objectifs, la sémantique et la vérification formelle des compositions et le cadre offert par l'ingénierie système. Cette thèse propose une démarche originale établissant les fondements théoriques et méthodologiques pour un processus sans rupture entre ingénierie système, optimisation multi-objectif et simulation multi-physique. Des cas d'études issus de l'automobile démontrent la validité de cette approche expérimentée sur la base du langage Modelica. / Multi-disciplinary and multi-physics simulation represents a major scientific and industrial challenge. The simulation has essentially been considered by physicists (mechanic domain, electromagnetic domain, ...) as a numerical problem on specific case studies but has never been adressed from a system perspective. The general problem induced by the numerical simulation of complex systems include model composition, multi-objective optimization, the semantics and formal verification of compositions and the frame of systems engineering. This thesis proposes an original approach establishing the theoretical and methodological foundations for a seamless process between systems engineering, multi-objective optimization and multi-physics simulation. Automotive case studies show the validity of such an approach based on Modelica langage.

Studiens syfte var att studera hur första- och andraspråkstalande studenter agerar i den akademiska gemenskapen med fokus på hur de inkorporerar röster genom att referera och citera. Studien samlade in data genom enkäter och texter som sedan användes för analys. Urvalet bestod av 10 deltagare varav 5 var svenska som förstaspråkstalare och 5 svenska som andraspråkstalare. Deltagarna var inskrivna och gick kursen Akademiskt skrivande 1SV108 på Linneuniversitetet. De viktigaste resultaten studien fann var att det fanns en individuell variation i val och användning av inkorporering av röster i akademisk skrift. Den individuella variationen bestod av vilka referensmarkörer som användes för att inkorporera källor och skribenternas egna röster och hur och vilka typer av citat som användes för att uttrycka skribentens röst.

The diploma thesis deals with solution of construction commercial and administrative building in Ostrava. The general aim is realization of building foundition. This work also deals with studies of the building. Building is located in the center of Ostrava on a flat terrain. The components of this thesis are technological specification, project construction site, schedule of work, financial plan and rough construction cost.

This thesis is aimed to specify and implement multi-purpose framework able to deal with graphical real-time system specification. This tool allows to use arbitrary verification approach to resulting system model check. Description of basic formal specification methods based on mathematic logic is done. Some well-known hierarchical graphical specifications for real-time systems are depictured. Author proposed suitable cases for functionality examination of resulting framework.

Hämatopoetische Stammzellen besitzen die Fähigkeit, die dauerhafte Erhaltung ihrer eigenen Population im Knochenmark zu gewährleisten und gleichzeitig zur Neubildung der verschiedenen Zelltypen des peripheren Blutes beizutragen. Die Sequenz von Entscheidungsprozessen, die den Übergang einer undifferenzierten Stammzelle in eine funktionale ausgereifte Zelle beschreibt, wird als Linienspezifikation bezeichnet. Obwohl viele Details zu den molekularen Mechanismen dieser Entscheidungsprozesse mittlerweile erforscht sind, bestehen noch immer große Unklarheiten, wie die komplexen phänotypischen Veränderungen hervorgerufen und reguliert werden. Im Rahmen dieser Dissertation wird ein geeignetes mathematisches Modell der Linienspezifikation hämatopoetischer Stammzellen entwickelt, welches dann in ein bestehendes Modell der hämatopoetischen Stammzellorganisation auf Gewebsebene integriert wird. Zur Verifizierung des theoretischen Modells werden Simulationsergebnisse mit verschiedenen experimentellen Daten verglichen. Der zweite Teil dieser Arbeit konzentriert sich auf die Beschreibung und Analyse der Entwick- lungsprozesse von Einzelzellen, die aus diesem integrierten Modell hervorgehen. Aufbauend auf den entsprechenden Modellsimulationen wird dazu eine topologische Charakterisierung der resultierenden zellulären Genealogien etabliert, welche durch verschiedener Maße für deren Quantifizierung ergänzt wird. Das vorgestellte mathematische Modell stellt eine neuartige Verknüpfung der intrazellulären Linienspezifikation mit der Beschreibung der hämatopoetischen Stammzellorganisation auf Populationsebene her. Dadurch wird das Stammzellm- odell von Röder und Löffler um die wichtige Dimension der Linienspezifikation ergänzt und damit in seinem Anwendungsbereich deutlich ausgedehnt. Durch die Analyse von Einzelzellverläufen trägt das Modell zu einem grundlegenden Verständnis der inhärenten Heterogenität hämatopoetischer Stammzellen bei.

This thesis is about coalgebraic methods in software specification and verification. It extends known techniques of coalgebraic specification to a more general level to pave the way for real world applications of software verification. There are two main contributions of the present thesis: 1. Chapter 3 proposes a generalisation of the familiar notion of coalgebra such that classes containing methods with arbitrary types (including binary methods) can be modelled with these generalised coalgebras. 2. Chapter 4 presents the specification language CCSL (short for Coalgebraic Class Specification Language), its syntax, its semantics, and a prototype compiler that translates CCSL into higher-order logic. / Die Dissertation beschreibt coalgebraische Mittel und Methoden zur Softwarespezifikation und -verifikation. Die Ergebnisse dieser Dissertation vereinfachen die Anwendung coalgebraischer Spezifikations- und Verifikationstechniken und erweitern deren Anwendbarkeit. Damit werden Softwareverifikation im Allgemeinen und im Besonderen coalgebraische Methoden zur Softwareverifikation der praktischen Anwendbarkeit ein Stück nähergebracht. Diese Dissertation enthält zwei wesentliche Beiträge: 1. Im Kapitel 3 wird eine Erweiterung des klassischen Begriffs der Coalgebra vorgestellt. Diese Erweiterung erlaubt die coalgebraische Modellierung von Klassenschnittstellen mit beliebigen Methodentypen (insbesondere mit binären Methoden). 2. Im Kapitel 4 wird die coalgebraische Spezifikationssprache CCSL (Coalgebraic Class Specification Language) vorgestellt. Die Bescheibung umfasst Syntax, Semantik und einen Prototypcompiler, der CCSL Spezifikationen in Logik höherer Ordnung (passend für die Theorembeweiser PVS und Isabelle/HOL) übersetzt.

Formal methods play an important part in the development as well as testing stages of software and hardware systems. A significant and often overlooked part of the process is the development of specifications and correctness requirements for the system under test. Traditionally, English has been used as the specification language, which has resulted in verbose and difficult to use specification documents that are usually abandoned during product development. This research focuses on investigating the use of Live Sequence Charts (LSCs), a graphical and intuitive language directly suited for expressing communication behaviors of a system as the specification language for a system under test. The research presents two methods for using LSCs as a specification language: first, by translating LSCs to temporal logic, and second, by translating LSCs to an automaton structure that is directly suited for formal verification of systems. The research first presents the translation for each method and further, identifies the pros and cons for each verification method.

Construction zones can greatly affect the traffic flow on roadways, especially when lane closures are required. Traditionally, the Utah Department of Transportation (UDOT) has used traffic management specifications that only allow lane closures and road work to be done during predetermined hours or specifications that require a certain number of lanes to be open at all times. Recently, mobility-based work-zone traffic flow maintenance has been considered. This method requires continuous monitoring of mobility-based performance data and a mechanism to send alerts to the contractors when the mobility data does not meet the standards set by the specifications. UDOT recently tested mobility-based performance specifications at an urban arterial work zone and studied issues related to implementation of mobility-based performance specifications. Parallel to this experiment, UDOT funded a study to develop guidelines for implementing mobility-based performance specifications to manage traffic flow in work zones. Dynamically collecting mobility-based data such as travel time and speed is now feasible using technologies such as Bluetooth and microwave sensors. The core benefit of using mobility-based performance specifications is that they can give the contractor more flexibility in construction work scheduling while maintaining an acceptable level of traffic flow. If the level of traffic flow is not maintained, then the contractor is assessed a financial penalty. The penalty is determined by the amount of time where the flow is not maintained at a predetermined condition. To discuss issues and develop guidelines, a task force consisting of UDOT representatives, several representatives from the construction industry, and researchers from Brigham Young University was formed. Through three task force meetings, a set of 12 guidelines were developed, including guidelines about when mobility-based performance specifications should be used and which mobility data should be used. Some of the issues were difficult for the task force members to agree on, and a decision-making theory called the Technique for Order Preference by Similarity to Ideal Solution (TOPSIS) was used to find best approaches to deal with some of the difficult issues associated with the implementation of mobility-based performance specifications in highway construction contracts. These guidelines should be reviewed as appropriate in the future as UDOT accumulates experience in using these types of specifications.