Discrete-Event systems (DES) is a framework in which problems are modelled as finite-state automata and a solution in the form of a supervisory control scheme can be automatically synthesized via an exhaustive search through the state space of the system. Various extensions to the standard DES framework have been introduced to allow it to be applied to a greater variety of problems. When the system in question is very large or varies with time, a limited lookahead policy can be adopted, in which control decisions are made on-the-fly by looking at finite-step projections of the behaviour of the system's underlying automata. This work presents a new approach to limited lookahead supervision which incorporates many of the extensions to DES that are already present in the literature, such as event probability and string desirability. When dealing with a limited lookahead technique, the projected system behaviour is represented as a lookahead tree with some depth limit decided on by the user. It can be difficult to strike a balance between the complexities associated with storing and analyzing the trees and the amount of information available to make decisions, both of which increase with depth. This work also presents a set of methods which are designed to aid in accurately estimating the state space of lookahead trees with the intent of simplifying the process of determining a favourable depth to use. Finally, the approaches introduced herein are applied to a simulation of an infectious disease outbreak, primarily to showcase them in action, but also for the possibility of illuminating any useful information for real-world health units. / Thesis (Master, Computing) -- Queen's University, 2012-01-20 19:35:58.007

To understand the processes affecting the abundance of wild populations is a fundamental goal of ecology and a prerequisite for the management of living resources. Variable abundance, however, makes the investigation of ecological processes challenging. Recruitment, the process whereby new individuals enter a given stage of a ?sh population, is a highly variable entity. I have confronted this issue by developing methodologies speci?cally designed to account for, and ecologically interpret, patterns of variability in recruitment. To provide the necessary context, Chapter 2 begins with a review of the history of recruitment science. I focus on the major achievements as well as present limitations, particularly regarding environmental drivers. Approaches that include explicit environmental information are contrasted with time-varying parameter techniques. In Chapter 3, I ask what patterns of variability in pre-recruit survival can tell us about the strength of density-dependent mortality. I provide methods to investigate the presence of density-dependent mortality where this has previously been hindered by highly variable data. Stochastic density-independent variability is found to be attenuated via density dependence. Sources of recruitment variability are further partitioned in Chapter 4. Using time-varying parameter techniques, signi?cant temporal variation in the annual reproductive rate is found to have occurred in many Atlantic cod populations. Multivariate state space models suggest that populations in close proximity typically have a shared response to environmental change whereas marked differences occur across latitude. Hypotheses that could result in consistent changes in productivity of cod populations are tested in Chapter 5. I focus on a meta-analytical investigation of potential interactions between Atlantic cod and small pelagic species, testing aspects of the cultivation-depensation hypothesis. The ?ndings suggest that predation or competition by herring and mackerel on egg and larval cod could delay recovery of depleted cod populations. Chapter 6 concludes with a critical re?ection on: the suitability of the theories employed, the underlying assumptions of the empirical approaches, and the quality of the data used in my thesis. Application of ecological insights to ?sheries management is critically evaluated. I then propose future work on recruitment processes based on methods presented herein.

The idea of performing power systems dynamic analysis in the power-angle domain has been hinted at by previous researchers, but this may be the first published document to develop detailed techniques by which entire power systems can be represented and solved in the power-angle domain. With the widespread deployment of phasor measurement units and frequency data recorders the industry is looking for more real-time analytical tools to turn real-time wide-area measurements into useful information. Applications based on power-angle domain analysis are simple enough that they may be used online. Power-angle domain analysis is similar to DC load-flow techniques in that a flat voltage profile is used and it is assumed that real power and voltage angle are completely decoupled from reactive power and voltage magnitude. The linearized equations for the dynamics of generators and loads are included in the model, which allows the electromechanical response to be solved using conventional circuit analysis techniques. The effect of generation trips, load switching, and line switching can be quickly approximated with nodal analysis or mesh analysis in the power-angle domain. The analysis techniques developed here are not intended to be as accurate as time-domain simulation, but they are simpler and fast enough to be put online, and they also provide a better analytical insight into the system. Power-angle domain analysis enables applications that are not readily available with conventional techniques, such as the estimation of electromechanical propagation delays based on system parameters, the formulation of electromechanical equivalents, modal analysis, stability analysis, and event location and identification based on a small number of angle or frequency measurements. Fault studies and contingency analysis are typically performed with detailed time-domain simulations, where the electromechanical response of the system is a function of every machine in the interconnection and the lines connecting them. All of this information is rarely known for the entire system for each operating condition; as a result, for many applications it may be more suitable to compute an approximation of the system response based on the current operating state of only the major lines and generators. Power-angle domain analysis is adept at performing such approximations. / Ph. D.

Gegenstand der Arbeit ist die Verifikation von verteilten diskreten Systemen in bezug auf Spezifikationen ihres Verhaltens. Diskrete Systeme bestehen aus einer abzaehlbaren Zustandsmenge und einer Zustandsuebergangsrelation. Bei verteilten Systemen ist eine signifikante Zahl von Zustandsuebergaengen nur durch eine kleine Zahl von Komponenten eines strukturierten Zustandsraumes bedingt und aendert auch nur wenige Komponenten. Bei praktisch relevanten Systemen ist die Zustandszahl unbeherrschbar gross. Dieses Phaenomen wird Zustandsraumexplosion genannt. Verteiltheit gilt als eine der wesentlichen Ursachen fuer Zustandsraumexplosion, weil nebenlaeufig moegliche lokale Zustandsuebergaenge abhaengig von ihren exponentiell vielen Ausfuehrungsreihenfolgen exponentiell viele verschiedene Zwischenzustaende erzeugen koennen. Fuer Verifikationsaufgaben sind Systeme daher implizit gegeben durch eine Beschreibung von Anfangszustaenden und (lokale) Regeln zur Generierung von Folgezustaenden. Solche Systembeschreibungen folgen verschiedenen Paradigmen, z.B. dem variablenorientierten Paradigma (Zustaende sind Werte von Variablen, die durch Zustandsuebergaenge gelesen und geschrieben werden) oder dem ressourcenorientierten Paradigma (Zustaende sind Verteilungen von Ressourcen im System, die durch Zustandsuebergaenge konsumiert oder produziert werden). Die Verfuegbarkeit von Verifikationstechniken oder spezifischen Implementationen haengt vom zugrundeliegenden Paradigma ab. Als Sprache zur Formulierung von Spezifikationen des Verhaltens verwenden wir etablierte temporale Logiken und fuer die Praxis bedeutsame Fragmente solcher Logiken. Temporale Logik beschreibt Eigenschaften von Abfolgen von Zustaenden, basierend auf elementaren, einzelne Zustaende betreffenden Eigenschaften. Auf einer expliziten Systemdarstellung lassen sich temporallogische Eigenschaften effizient, d.h. mit einer linear von der Zustandszahl abhaengigen Laufzeit, verifizieren. Eine solche Verifikation basiert auf einfachen Suchalgorithmen in dem durch das System definierten Zustandsgraph. Ein solcher Verifikationsansatz ist aber wegen der genannten Zustandsraumexplosion nicht durchfuehrbar. Im wesentlichen werden drei Loesungsansaetze in Richtung durchfuehrbarer Verifikationsalgorithmen verfolgt. Die strukturelle Verifikation versucht, Eigenschaften direkt aus spezifischen Mustern in der impliziten Systembeschreibung abzuleiten. Der derzeitige Stand der Technik gestattet solche Ableitungen nur fuer wenige und einfach strukturierte Verhaltensspezifikationen und erfordert auch dann in einigen Faellen recht aufwendige Berechnungen. Bei der symbolischen Zustandsraumanalyse wird der Zustandsraum erschoepfend durchmustert, allerdings unter Benutzung von Datenstrukturen, deren elementare Objekte ganze Mengen von Zustaenden beschreiben, und deren elementare Operationen die Folgezustaende fuer ganze solche Mengen aus der impliziten Systembeschreibung errechnen. Bei der expliziten Zustandsraumverifikation, dem Thema der vorliegenden Habilitationsschrift, wird eine explizite Repraesentation eines Zustandsraumes generiert, der wesentlich kleiner ist als der Zustandsraum des untersuchten Systems, in bezug auf die untersuchte Eigenschaft aber per Konstruktion aequivalent zum originalen System ist. Zur Konstruktion werden Informationen aus der impliziten Systembeschreibung herangezogen. Eine Technologie zur expliziten Zustandsraumverifikation besteht also aus - Einer mathematisch fundierten Theorie, die einer bestimmten Konstruktionsmethode bescheinigt, welche Eigenschaften durch sie bewahrt werden; - effizienten Algorithmen zur Implementation eine solchen Konstruktion; Die Arbeit enthaelt, fuer mehrere bekannte Verfahren, Beitraege zu jeweils mindestens einem der beiden Bestandteile einer expliziten Zustandsraumverifikationstechnik. Die Methode der sturen Mengen verkleinert den explizit zu konstruierenden Zustandsraum dadurch, dass von den in einem Zustand moeglichen Zustandsuebergaengen nur einige tatsaechlich untersucht werden, so dass weit weniger Zwischenzustaende durch verschiedene Abfolge nebenlaeufiger lokaler Zustandsuebergaenge entstehen. Die zu untersuchenden Uebergaenge werden abhaengig von der zu verifizierenden Eigenschaft und Informationen aus der Systemstruktur so ausgewaehlt, dass zu jeder Klasse von fuer die Eigenschaft relevanten Systemablaeufen wenigstens einer im reduzierten Zustandsraum repraesentiert ist. Die erste 1988 veroeffentlichte Methode diente der Bewahrung von terminalen Zustaenden sowie mindestens eines Pfades unendlicher Laenge. In der Folge wurde diese Technik auf viele andere Klassen von Eigenschaften erweitert, wobei vor allem die Faehigkeit, einen unendlichen Pfad zu bewahren, dahingehend verfeinert wurde, dass gezielt Pfade mit bestimmten Eigenschaften bewahrt werden konnten. Dabei spielte das Konzept unsichtbarer Zustandsuebergaenge eine tragende Rolle, wobei ein unsichtbarer Zustandsuebergang die Eigenschaft hat, dass er keine fuer die Eigenschaft relevanten Zustandskomponenten aendert. Daher war die Anwendung der Methode sturer Mengen begrenzt auf lokale Systemeigenschaften, weil andereseits zu wenige unsichtbare Uebergaenge fuer eine substantielle Reduktion zur Verfuegung stuenden. In der vorliegenden Arbeit setzen wir an der ersten Arbeit zur Methode sturer Mengen an und verfeinern die Faehigkeit, terminale Zustaende zu bewahren, dahingehend, dass nun die Praesenz von Zustaenden mit beliebigen in temporaler Logik formulierbaren Eigenschaften bewahrt werden. Die neue Methode basiert nicht auf der Existenz unsichtbarer Uebergaenge und kann in der Tat auch bei der Verifikation globaler Systemeigenschaften zu substantieller Reduktion fuehren. Das neue Konzept zur Konstruktion des reduzierten Zustandsraumes sind sogenannte UP-Mengen. Eine UP-Menge ist eine Menge von Uebergaengen, von denen mindestens einer in einem Systemablauf von einem Zustand, der die untersuchte Eigenschaft nicht erfuellt, zu einem Zustand, der die Eigenschaft erfuellt, vorkommen muss. Wir geben Algorithmen an, die kleine UP-Mengen fuer beliebige Zustaende aus der impliziten Systembeschreibung und einer Repraesentation der untersuchten Eigenschaft in der temporalen Logik CTL berechnet. Wir zeigen, dass jede Konstruktion, die in einem Zustand alle Uebergaenge in einer schwach sturen Obermenge einer zu dem Zustand berechneten UP-Menge untersucht, alle Zustaende erreicht, die die Eigenschaft besitzen. Dabei ist die Konstruktion schwach sturer Mengen die allen Methoden sturer Mengen gemeinsame Grundkonstruktion. Symmetrische Reduktion verkleinert den zu untersuchenden Zustandsraum dadurch, dass zu jeder Klasse von in bezug auf Symmetrie aequivalenten Zustaenden jeweils nur einer weiterverfolgt wird. Dadurch lassen sich alle gegenueber Symmetrie insensitive Eigenschaften bewahren (wobei man oft Insensitivitaet einer Eigenschaft durch die geeignete Wahl der Symmetrienmenge erreichen kann). Symmetrische Reduktion beinhaltet zwei Probleme, erstens das Aufinden der einem System innewohnenden Symmetrie, und zweitens, zu einem gegebenen Zustand, das Auffinden zu ihm aequivalenter Zustaende in der Menge bereits untersuchter Zustaende. Die meisten vorhandenen Implementationen leiten Symmetrien aus speziellen Datenstrukturen ab, in denen wegen der eingeschraenkten Operationen die verschiedenen Elemente des Typs austauschbar sind. Das Auffinden aequivalenter Zustaende wird durch eine Transformation neu berechnter Zustaende in einen aequivalenten kanonischen Repraesentanten realisert. Alternativ zu diesem Ansatz wurde zur Beschreibung von Symmetrien die Verwendung von Graphautomorphismen auf netzartigen impliziten Systembeschreibungsformen vorgeschlagen. Es zeigt sich, dass per Umwandlung von Datenabhaengigkeiten in Graphrepraesentationen, jede Datentypsymmetrie auch einen Graphautomorphismus bildet, andererseits aber durch Graphautomorphismen Symmetrien beschreibbar sind, die sich in Datentypbetrachtungen nicht wiederfinden lassen. Diese zusaetzlichen Symmetrien erlauben eine staerkere Reduktion des Zustandsraumes. Zur Graphautomorphismentechnik fehlten bislang leistungsfaehige Algorithmen zur Umsetzung dieser Technologie. Wir setzen an der auf Graphautomorphismen basierenden Methode an und unterlegen alle Teilprobleme mit leistungsfaehigen Algorithmen. Die Berechnung der Automorphismen beschraenken wir auf ein Erzeugendensystem, das polynomiell viele Elemente, gemessen an der Groesse der impliziten Systembeschreibung, hat. Die Berechnung selbst ist schlimmstenfalls exponentiell, was nicht verwundert, weil das Problem mit einem Entscheidungsproblem eng korreliert, von dem bekannt ist, dass es in der Klasse NP, aber unbekannt, ob es NP-vollstaendig oder in P liegt. Diese Eigenschaft hat dem Problem eingehende Untersuchung zuteil werden lassen, wegen der nach wie vor offenen "P ungleich NP?"-Frage. Trotzdem ist kein polynomieller Algorithmus bekannt. Umso erfreulicher ist es, dass unser Berechnungsalgorithmus sich auf realistischen Beispielen bisher durchweg polynomiell verhielt, und lediglich bei eigens konstruierten Systemen ins Exponentielle ausriss. Fuer die Loesung des Problems, aequivalente bereits bekannte Zustaende aufzuspueren, schlagen wir mehrere Techniken vor und beschreiben ihre Leistungsfaehigkeit abhaengig von der Struktur der innewohnenden Symmetrie. Fuer duenne Symmetriegruppen (wenige symmetrische Transformationen) eignet sich eine Technik, bei der die Symmetrien der Reihe nach aus dem Erzeugendensystem generiert werden, und das symmetrische Bild des neuen Zustandes mit der Menge der bekannten Zustaende verglichen wird. Dabei koennen wir, abhaengig vom Ausgang einer solchen Ueberpruefung, die Generierung von Symmetrien unterdruecken, von denen aus vorhandenen Informationen klar ist, dass sie keinesfalls zum Erfolg fuehren. Dadurch kann eine erhebliche Effizienzsteigerung erzielt werden. Bei einer zweiten Technik iterieren wir die bekannten Zustaende, genauer gesagt, diejenigen Zustaende, die fuer eine die Symmetrie respektierende Hashfunktion denselben Wert liefert wie der neue Zustand, ob es eine Symmetrie gibt, die beide Zustaende ineinander ueberfuehrt. Das verbleibende Problem kann durch eine Adaption des Symmetrieberechnungsverfahrens geloest werden. Eine vorherige Berechnung des Erzeugendensystems kann entfallen. Die dritte vorgeschlagene Technik benutzt das Erzeugendensystem, um den neuen Zustand approximativ in einen kanonischen aequivalenten Zustand zu ueberfuehren. Diese Technik ist von allen beschriebenen Methoden die effizienteste, liefert aber groessere Zustandsraeume als die beiden anderen Techniken. Wir studieren die Vor- und Nachteile aller Techniken anhand mehrerer Beispielsysteme. Die dritte in der Arbeit behandelte Technik ist die Methode der Ueberdeckbarkeitsgraphen. Sie ist spezifisch fuer die ressourcenbasierte Systembeschreibungsform der Petrinetze. Sie diente urspruenglich zur Aufspuerung von Stellen im System, an denen sich unbeschraenkt viele Ressourcen ansammeln koennen. Formal ist ein Ueberdeckbarkeitsgraph eine endliche Abstraktion eines Systems mit bis zu unendlich vielen Zustaenden. Von nur wenigen Eigenschaften war bekannt, dass sie sich aus dem Ueberdeckbarkeitsgraphen ableiten lassen. Wir formulieren Regeln zur Auswertung von Ueberdeckbarkeitsgraphen, mit deren Hilfe es moeglich ist, eine Vielzahl von in temporaler Logik formulierten Eigenschaften aus dem Ueberdeckbarkeitsgraph abzuleiten. Diese Reglen sind inhaerent unvollstaendig, da bekannt ist, dass fuer viele Eigenschaften es Paare von Systemen gibt, die isomorphe Ueberdeckbarkeitsgraphen liefern, sich aber in bezug auf die Eigenschaft verschieden verhalten. Fuer universelle Eigenschaften des CTL-Fragments ACTL erhalten wir Bewahrungsresultate durch das Ausweisen einer Simulationsrelation zwischen dem originalen System und seinem Ueberdeckbarkeitsgraph. Fuer existentielle Eigenschaften basieren unsere Resultate auf einer Abschwaechung der Erfuellbarkeitsrelation ueber Zustaenden des Ueberdeckbarkeitsgraphen. Einem Zustand des Ueberdeckbarkeitsgraphen entsprechen divergierende Folgen von Zustaenden des Originalgraphen. Normalerweise schreibt man einem Zustand des Ueberdeckbarkeitsgraphen dann eine Eigenschaft zu, wenn alle Folgenglieder im Originalsystem die Eigenschaft besitzen. Wir arbeiten dagegen mit einem Begriff, wo Gueltigkeit der Eigenschaft nur fuer fast alle Folgenglieder gefordert wird. Eine letzte Gruppe von Techniken ist bisher in der Zustandsraumverifikation nicht eingestzt worden, aber aus der strukturellen Verifikation fuer Petrinetze bekannt. Zu einem Petrinetz kann eine ganzzahlige Inzidenzmatrix C gebildet werden, mit deren Hilfe ein linear-algebraischer Zusammenhang zwischen voneinander errichbaren Zustaenden hergestellt werden kann. Stellen- und Transitionsinvarianten sind Loesungen der durch C-T bzw. C definierten homogenen Gleichungssysteme. Dabei dienen Stelleninvarianten gewoehnlich einer Abschaetzung der Menge der erreichbaren Zustaende nach oben, mit daraus resultierenden Moeglichkeiten der Ableitung von Eigenschaften, waehrend Transitionsinvarianten Zyklen im Zustandsraum charakterisieren. Wir verwenden Stelleninvarianten zur Kompression von einzelnen Zustaenden. Durch Stelleninvarianten lassen sich einige Komponenten in einen funktionalen Zusammenhang zu den verbleibenden Komponenten stellen. Dadurch ist auch nach dem Streichen der funktional abhaengigen Stellen der Zustand noch eindeutig determiniert. Wir zeigen, dass bei der Konstruktion des Zustandsraumes ein durch die verbleibenden Stellen gebildeter "Fingerabdruck" ausreicht. Transitionsinvarianten verwenden wir dazu, eine Menge von Zustaenden so auszuzeichnen, dass jeder Zyklus im Zustandsraum mindestens einen ausgezeichneten Zustand enthaelt. Darufhin speichern wir noch noch ausgezeichnete Zustaende permanent, sparen also Speicherplatz. Fuer nicht ausgezeichnete Zustaende kann es passieren, dass sie mehrmals aufgesucht werden (auf verschiedene Weise aus Vorgaengerzustaenden entstehen). Weil sie nicht gespeichert sind, werden auch wiederholt ihre Nachfolgezustaende untersucht. Da in jedem Kreis mindestens ein ausgezeichneter, also permanent zu speichernder Zustand enthalten ist, entstehen durch diese wiederholte Berechnung keine Probleme in bezug auf Terminierung des Verfahrens, wohl aber erhebliche Laufzeiteinbussen. Wir schlagen Methoden zur Begrenzung der Laufzeiteinbussen um den Preis weiterer zu speichernder Zustaende vor. Fuer alle untersuchten Methoden studieren wir die Abhaengigkeit der Anwendbarkeit und Effizienz der Methode von dem der gegebenen impliziten Systembeschreibung zugrundeliegenden Paradigma. Wir untersuchen ebenfalls die Kompatibilitaet der Verfahren mit verschiedenen Strategien zur Generierung des Zustandsraumes (Tiefe zuerst, Breite zuerst, verteilt) und Moeglichkeiten der gemeinsamen Anwendung verschiedener Techniken. / Verification is the task of determining whether a (model of a) system holds a given behavioral property. State space verification comprises a class of computer aided verification techniques where the property is verified through exhaustive exploration of the reachable states of the system. Brute force implementations of state space verification are intractable, due to the well known state explosion problem. Explicit state space verification techniques explore the state space one state at a time, and rely usually on data structures where the size of the data structure increases monotonously with an increasing number of explored states. They alleviate state explosion by constructing a reduced state space that, by a mathematically founded construction, behaves like the original system with respect to the specified properties. Thereby, decrease of the number of states in the reduced system is the core issue of a reduction technique thus reducing the amount of memory required. An explicit state space verification technique comprises of - a theory that establishes whether, and how, certain properties can be preserved through a construction of a reduced state space; - a set of procedures to execute the actual construction efficiently. In this thesis, we contribute to several existing explicit state space verification techniques in either of these two respects. We extend the class of stubborn set methods (an instance of partial order reduction) by constructions that preserve previously unsupported classes of properties. Many existing constructions rely on the existence of "invisible" actions, i.e. actions whose effect does not immediately influence the verified property. We propose efficient constructions that can be applied without having such invisible actions, and prove that they preserve reachability properties as well as certain classes of more complex behavioral system properties. This way, so called "global" properties can now be approached with better stubborn set methods. We pick up a graph automorphism based approach to symmetry reduction and propose a set of construction algorithms that make this approach feasible. In difference to established symmetry techniques that rely on special "symmetry creating" data types, a broader range of symmetries can be handled with our approach thus obtaining smaller reduced state spaces. Coverability graph construction leads to a finite representation of an infinite state space of a Petri net by condensing diverging sequences of states to their limit. We prove rules to determine temporal logic properties of the original system from its coverability graph, far beyond the few properties known to be preserved so far. We employ the Petri net concept of linear algebraic invariants for compressing states as well as for leaving states out of explicit storage. Compression uses place invariants for replacing states by smaller fingerprints that still uniquely identify a state (unlike many hash compression techniques). For reducing the number of explicitly stored states, we rely on the capability of Petri net transition invariants to characterize cycles in the state space. For termination of an exhaustive exploration of a finite state space, it is sufficient to cover all cycles with explicitly stored states. Both techniques are easy consequences of well known facts about invariants. As a novel contribution, we observe that both techniques can be applied without computing an explicit representation of (a generating set for) the respective invariants. This speeds up the constructions considerably and saves a significant amount of memory. For all presented techniques, we illustrate their capabilities to reduce the complexity of state space reduction using a few academic benchmark examples. We address compatibility issues, i.e. the possibility to apply techniques in combination, or in connection with different strategies for exploring the reduced state space. We propose a scheme to distribute state space exploration on a cluster of workstations and discuss consequences for using this scheme for state space reduction. We collect observations concerning the impact of the choice of system description formalisms, and property specification languages, on the availability of explicit state space verification techniques.

The discipline of component-based modeling and simulation offers promising gains including reduction in development cost, time, and system complexity. This paradigm is very profitable as it promotes the use and reuse of modular components and is auspicious for effective development of complex simulations. It however is confronted by a series of research challenges when it comes to actually practice this methodology. One of such important issue is Composability verification. In modeling and simulation (M&amp;S), composability is the capability to select and assemble components in various combinations to satisfy specific user requirements. Therefore to ensure the correctness of a composed model, it is verified with respect to its requirements specifications.There are different approaches and existing component modeling frameworks that support composability however in our observation most of the component modeling frameworks possess none or weak built-in support for the composability verification. One such framework is Base Object Model (BOM) which fundamentally poses a satisfactory potential for effective model composability and reuse. However it falls short of required semantics, necessary modeling characteristics and built-in evaluation techniques, which are essential for modeling complex system behavior and reasoning about the validity of the composability at different levels.In this thesis a comprehensive verification framework is proposed to contend with some important issues in composability verification and a verification process is suggested to verify composability of different kinds of systems models, such as reactive, real-time and probabilistic systems. With an assumption that all these systems are concurrent in nature in which different composed components interact with each other simultaneously, the requirements for the extensive techniques for the structural and behavioral analysis becomes increasingly challenging. The proposed verification framework provides methods, techniques and tool support for verifying composability at its different levels. These levels are defined as foundations of a consistent model composability. Each level is discussed in detail and an approach is presented to verify composability at that level. In particular we focus on theDynamic-Semantic Composability level due to its significance in the overallcomposability correctness and also due to the level of difficulty it poses in theprocess. In order to verify composability at this level we investigate the application ofthree different approaches namely (i) Petri Nets based Algebraic Analysis (ii) ColoredPetri Nets (CPN) based State-space Analysis and (iii) Communicating SequentialProcesses based Model Checking. All the three approaches attack the problem ofverifying dynamic-semantic composability in different ways however they all sharethe same aim i.e., to confirm the correctness of a composed model with respect to itsrequirement specifications. Beside the operative integration of these approaches inour framework, we also contributed in the improvement of each approach foreffective applicability in the composability verification. Such as applying algorithmsfor automating Petri Net algebraic computations, introducing a state-space reductiontechnique in CPN based state-space analysis, and introducing function libraries toperform verification tasks and help the molder with ease of use during thecomposability verification. We also provide detailed examples of using each approachwith different models to explain the verification process and their functionality.Lastly we provide a comparison of these approaches and suggest guidelines forchoosing the right one based on the nature of the model and the availableinformation. With a right choice of an approach and following the guidelines of ourcomponent-based M&amp;S life-cycle a modeler can easily construct and verify BOMbased composed models with respect to its requirement specifications. / <p>Overseas Scholarship for PHD in selected Studies Phase II Batch I</p><p>Higher Education Commision of Pakistan.</p><p>QC 20130224</p>