Dissertations / Theses on the topic 'Formal and semi-formal notation'

Business Process Modelling Notation (BPMN) is a standardised diagram notation for modelling interactive workflow processes graphically at the design stage. The primary objective of this thesis is to provide a framework for precise specifications and formal verifications of workflow processes modelled as BPMN diagrams. We provide two behavioural semantics for BPMN in the process algebra Communicating Sequential Processes (CSP). We apply existing CSP refinement orderings to both the refinement of business process diagrams and the verification of behavioural compatibility of business process collaborations. The first semantic model is an untimed model, focusing on the control flow and communication of business processes. The second semantic model extends the first one to capture the timing aspect of behaviour. We also consider the applications of the semantic models. The secondary objective of this thesis is to apply BPMN and the semantic models to reason about long running empirical studies (e.g. laboratory experiments, clinical trials). We introduce a declarative workflow model Empiricol for recording trials and experiments precisely, and define bidirectional transformation functions between BPMN and Empiricol. Using the transformation functions, we make graphical specification, simulation, automation and verification of trials and experiments possible. We provide two case studies on the applications of BPMN’s formalisations.

Les notations semi-formelles et formelles semblant complémentaires, leur couplage semble un cadre intéressant pour pouvoir bénéficier de leurs avantages respectifs tout en diminuant leurs points faibles. En effet, d'une part, les notations semi-formelles qui pêchent par leur précision sont de bons vecteurs de communication dont le coût de formation est raisonnable ; d'autre part, les langages formels apportent la précision et le potentiel de raisonnement manquant aux notations semi-formelles. Dans ce travail, nous proposons une approche de traduction de modèles semi-formels objet en des spécifications formelles en Z ou en Object-Z afin de fournir un couplage bénéfique de ces deux types de spécifications. Nous cherchons à rendre nos propositions les plus utilisables possible en en montrant trois bénéfices avérés : un guide méthodologique pour l'expression des contraintes annotant un modèle objet, une aide à la vérification des modèles et de leurs contraintes et des raisonnements informels sur la sémantique de modèles simples. Nous avons aussi développé un outil de support à notre approche, RoZ qui permet de faire cohabiter les notations semi-formelles et formelles. Enfin nous étudions une autre approche de couplage, la vérification de cohérence par méta-modélisation pour laquelle nous proposons des règles de cohérence entre le modèle objet et Z. Ce travail nous permet de comparer cette approche avec notre stratégie de traduction afin de mieux comprendre leurs avantages et leurs inconvénients<br>Semi-formal and formal notations being complementary, their joint use could define an interesting framework in order to take advantage of their good points by reducing their drawbacks. On the one hand, semi-formal notations which are imprecise are good communication vectors with affordable training cost ; on the other hand, formal languages bring precision and their reasoning abilities which miss to semi-formal notations. In this work, we propose a translation approach from semi-formal object models to formal specifications in Z and Object-Z so as to offer a powerful integration of these two kinds of specifications. We want to make our proposals the most useful possible by showing three established advantages : a methodological guidance to express constraints annotating an object model ; an help to check the models and their constraints and informal reasoning about the semantics of simple models. We also have developed a tool, RoZ that supports our approach by making semi-formal and formal notations live together. Finally, we study another integration approach, the consistency checking by meta-modelling for which we propose consistency rules between the object model and Z. This work enables us to compare this approach with our translation strategy to understand their advantages and drawbacks

Ce travail se situe dans le cadre de la recherche de systèmes de notation permettant de transcrire de façon symbolique l’aspect concret et sensoriel, et non seulement abstrait et structurel, des artefacts de la musique par ordinateur. Dans ce but, nous exposons tout d’abord un modèle formel complet et minimal des objets et structures audionumériques, en référence aux critères de la perception ; ce modèle est implémenté sous la forme d’un langage fonctionnel Turing-potent qui permet d’effectuer l’équivalence entre l’expression mathématique d’un signal et sa réalisation informatique. Puis, nous employons ce formalisme afin d’exprimer un ensemble de critères de synthèse sonore, ce qui donne lieu à un logiciel de synthèse dont l’expressivité est considérable. Ces outils sont organisés suivant le schéma des théories Schaefferiennes, par une décomposition catégorielle dans laquelle les paramètres correspondent à des notions morphologiques. Finalement, nous rendons compte d’une série d’expériences visant à évaluer la pertinence de ces critères dans l’audition humaine, avec le concours d’un musicologue, puis sur un ensemble de sujets, et enfin vis-à-vis d’un public aussi large que possible. Ceci nous conduit à remettre en question la méthodologie la plus adéquate pour traiter ce type de problème, qui nous rapproche des sciences humaines et sociales, et suggère une démarche de science participative<br>This piece of work is situated in the context of research on notation systems enabled to transcribe symbolically the concrete and sensorial aspect, and not only the abstract and structural aspect, of computer music artefacts. In this perspective, we first expose a complete and minimal formal model for digital audio objects and structures, relatively to the criteria of perception ; this model is implemented as a Turing-potent functional language, that draws the correspondance between the mathematical expression of a signal and its computational realisation. Then, we apply this formal construction to the expression of a number of schemes for sound synthesis, producing a software synthetiser whose expressivity is consequent. These tools are organised following the lines of Schaefferian theories, through a decomposition into categories whose parameters correspond with morphological notions. Finally, we draw the conclusions of a series of experiments aiming to evaluate the relevance of those schemes in human hearing, with the assistance of a musicologist, then with a number of subjects, and eventually by associating a public that is as wide as possible. This leads us to question the methodology most appropriate to tackle this kind of problem, which brings us closer to social science, and suggests a participative science approach

Especificações formais são úteis para descrever o que um sistema deve fazer sem definir como, e, em virtude da sua natureza formal e da possibilidade de abstração, é possível analisá-las sistematicamente. No entanto, o uso de especificações formais como parte do desenvolvimento de software não constitui prática comum. Isso se dá, em parte, pelo fato de existirem apenas um pequeno número de metodologias e ferramentas adequadas que dêem suporte a esse desenvolvimento. O primeiro objetivo deste trabalho é propor uma metodologia de desenvolvimento que possibilite, a partir de uma especificação formal em notação Z, produzir uma implementação dessa especificação em Java. Essa metodologia centra-se na geração do esqueleto da aplicação Java e na instrumentação desse esqueleto com mecanismos de verificação de condições (invariantes, pré e pós-condições) e rastreamento de violações dessas condições. Através desses mecanismos, possibilita-se intercalar desenvolvimento formal e informal no processo global de desenvolvimento de software. O segundo objetivo é desenvolver uma ferramenta que implemente parte dessa metodologia, produzindo uma implementação parcial que deverá ser complementada pelo usuário.<br>Formal specifications are useful for describing what a system should do, without defining how, and, owing to its formal nature, it is possible to analyse them systematically. However useful formal specifications are, their usage as part of the software development process is rather rare. This is, in part, due to the scarcity of both methodologies and tools that support this development. The first goal of this work is to define a software development methodology that enables the developer to produce a Java application from a formal specification written in Z. This methodology will rely strongly on the generation of Java application skeletons and instrumentation of the generated code with means of verifying conditions (invariants, pre and post-conditions) e tracing violations of these conditions. Through this mechanisms, it is possible to mix formal and informal development in the global software development process. The second goal of this work is to develop a tool that will implement part of this methodology, producing a partial implementation that must be complemented by the developer.

Thesis (Ph.D.)--Indiana University, Computer Science and Cognitive Science, 2007.<br>Title from PDF t.p. (viewed Nov. 11, 2008). Source: Dissertation Abstracts International, Volume: 68-09, Section: B, page: 6350. Advisers: Robert L. Goldstone; Michael Gasser.

Abstraction-guided simulation is a promising semi-formal framework for design validation in which an abstract model of the design is used to guide a logic simulator towards a target property. However, key issues still need to be addressed before this framework can truly deliver on it's promise. Concretizing, or finding a real trace from an abstract trace, remains a hard problem. Abstract traces are often spurious, for which no corresponding real trace exits. This is a direct consequence of the abstraction being an over-approximation of the real design. Further, the way in which the abstract model is constructed is an open-ended problem which has a great impact on the performance of the simulator. In this work, we propose a novel approaches to address these issues. First, we present a genetic algorithm to select sets of state variables directly from the gate-level net-list of the design, which are highly correlated to the target property. The sets of selected variables are used to build the Partition Navigation Tracks (PNTs). PNTs capture the behavior of expanded portions of the state space as they related to the target property. Moreover, the computation and storage costs of the PNTs is small, making them scale well to large designs. Our experiments show that we are able to reach many more hard-to-reach states using our proposed techniques, compared to state-of-the-art methods. Next, we propose a novel abstraction strengthening technique, where the abstract design is constrained to make it more closely resemble the concrete design. Abstraction strengthening greatly reduces the need to refine the abstract model for hard to reach properties. To achieve this, we efficiently identify sequentially unreachable partial sates in the concrete design via intelligent partitioning, resolution and cube enlargement. Then, these partial states are added as constraints in the abstract model. Our experiments show that the cost to compute these constraints is low and the abstract traces obtained from the strengthened abstract model are far easier to concretize.<br>Master of Science

Thesis (M.S. in Software Engineering) Naval Postgraduate School, Dec. 2000.<br>Thesis advisors, Neil Rowe, Man-Tak Shing. "December 2000." Includes bibliographical references (p. 101-102). Also available in print.

Assertion-based verification (ABV) is a powerful verification approach that has been proven to help digital IC architects, designers, and verification engineers improve design quality and reduce time to market.Assertions are a very powerful, concise and precise mechanism to specify properties of logic design. They run in all verification environments: simulation, emulation/acceleration and formal. In addition, they can be used as checkers or alternatively as assumptions.Some of the major challenges of ABV are that assertions are time-consuming to debug, there's no good way to measure the quality of hand-generated assertions and it's unclear how many assertions one needs to write.This thesis is an attempt at providing new ideas on how to resolve such issues. Different methods of adding assertions to an existing set have been explored and the task of writing enough assertions will be broken down into smaller and more manageable chunks. In order to do so, various types of assertions have first been identified in terms of their usefulness from the designers' and verification engineers' points of view.Lastly, the implementation of logic synthesis techniques to optimize assertions has been explored. Many significant improvements in terms of minimizing the total number of assertions as well as producing more efficient assertions have been observed.<br>La vérification basée sur l'assertion (Assertion-based Verification - ABV) est une approche de vérification puissante ayant été prouvée à aider les architectes numériques de circuits intégrés, les concepteurs et les ingénieurs de vérification à améliorer la qualité de conception et de réduire le temps de mise sur le marché. Les assertions sont un outil très puissant et précis pour définir les propriétés de la conception logique. Elles peuvent être employées dans tous les environnements de vérification: simulation, émulation ou formelle. Aussi important, elles peuvent être utilisées comme corrections ou encore comme hypothèses.Les inconvénients majeurs d'ABV sont que les assertions nécessitent beaucoup de temps a déboguer, qu'il n'y a pas de bonne facon de mesurer la qualité des assertions produites manuellement et qu'on ne sait pas comment déterminer combien d'assertions on a besoin d'écrire.Cette thèse tente d'apporter de nouvelles idées afin de résoudre ces questions. Différentes méthodes d'ajouter des assertions ont été explorées. La tache de la rédaction d'assez d'assertions a été décomposée en plus petits et plus gérables morceaux.Pour réaliser ceci, différents types d'assertions ont été d'abord identifiées en termes de leur utilité des points de vue des concepteurs et ingénieurs de vérification.Enfin, la mise en œuvre des techniques de synthèse logique pour optimiser les assertions ont été explorées. Des améliorations notables en termes de minimisation du nombre total d'assertions ainsi que la production d'assertions plus efficaces ont été observées.

Communication protocols play a central role in modern telecommunication systems. Protocols are developed to assure that a given service by a system can be provided to an end user in a reliable and efficient manner. The ever-growing influence of telecommunication and distributed systems over daily life require the protocols developed to be free from design errors. One can easily imagine the consequences of protocol failure in the automatic teller machines (ATM), the failure of protocols while making phone calls or failure of protocols in safety critical system such as nuclear power plants and aeroplanes. Any subtle design errors in these protocols can lead to expensive and dangerous consequences. The traditional methodologies such as simulation and design by intuition of protocols are already showing weaknesses and can no longer be relied upon in order to develop modern large complex communication and distribution systems. The formal methods are being deployed in the industry and research institute to develop protocols that are highly reliable and ideally do not contain any errors. Generally, speaking these formal methods can be divided into two categories namely analytic versus synthetic. The analytical methods to design protocols are relatively simple but by no mean guarantee the generation of protocols that are free from design errors. The methods used can only detect errors after the protocol has been designed by means of simulation and validation using automated tools. The synthetic methods allow the generation of protocols that are free from design errors using advanced discrete mathematical concepts and state theory. The complexity of the methods proposed makes it extremely difficult to use them for the protocol of even simplistic natures. The methods proposed so far as shown their usability to the protocol of academic nature only. A semi formal graphical method proposed by this study to design protocol suggest a synthesis method that uses formal graphical language to synthesis the protocols. It overcomes a number of difficulties that are present in formal synthetical methods and early results show that the method can be applied to the protocol of realistic nature. This method also has some weaknesses but it is hoped that future research in this area will overcome some of these.

The study of formal power series is an area of interest that spans many areas of mathematics. We begin by looking at single-variable formal power series with coefficients from a field. By restricting to those series which are invertible with respect to formal composition we form a group. Our focus on this group focuses on the classification of elements having finite order. The notion of a semi-cyclic group comes up in this context, leading to several interesting results about torsion subgroups of the group. We then expand our focus to the composition of multivariate formal power series, looking at similar questions about classifying elements of finite order. We end by defining a natural automorphism on this group induced by a group action of the symmetric group.

Welfare reform in middle income countries, where formal institutions conventionally have an exclusionary character and informal institutions are central to social welfare, has been marked by a drastic rise of means-tested social assistance schemes. This dissertation analyses, with an empirical focus on Turkey, the potential of these schemes to expand social rights by creating new formal entitlements for previously excluded groups. The number and the scope of social assistance schemes in Turkey have shown a remarkable increase, especially after the 2001 economic crisis, accompanied by significant institutionalisation. Yet, we argue that whilst social assistance has grown distinctively and become an integral part of the emerging welfare regime, certain characteristics of the previous regime were ultimately reproduced within new institutions due to the content of current schemes and the institutional structure of implementation. These include the association of mainstream welfare institutions with social insurance, the ambiguous role of the state towards the excluded parts of the society, the reliance on family relations and informal employment, and the prevalence of paternalist or clientelist motivations. Consequently, the potential of social assistance to extend formalised rights to the entire population was undermined, and the outcome has been the consolidation of a semi-formal welfare regime. To substantiate this argument, the dissertation develops a historical institutionalist framework and examines the elements of institutional change and continuity as well as the processes of change. Our three empirical chapters then focus on the development of legal, organisational, ideational and political bases of social assistance; trends in policy outcomes from the perspectives of decommodification, commodification, defamilialisation and declientelisation; and the functioning of social assistance through semi-autonomous foundations at the local level. Empirically, we build our argument on a comprehensive evidence base including a wide range of policy documents and qualitative interviews. Theoretically, we discuss the implications of our findings for the literatures on welfare regimes and institutionalism, stressing the importance of implementation structures, the co-existence of institutional change and continuity, and the suggestion of a semi-formal regime type.

Cette thèse présente le développement d'un framework formel pour la représentation des Langues de Signes (LS), les langages des communautés Sourdes, dans le cadre de la construction d'un système de reconnaissance automatique. Les LS sont de langues naturelles, qui utilisent des gestes et l'espace autour du signeur pour transmettre de l'information. Cela veut dire que, à différence des langues vocales, les morphèmes en LS ne correspondent pas aux séquences de sons; ils correspondent aux séquences de postures corporelles très spécifiques, séparés par des changements tels que de mouvements. De plus, lors du discours les signeurs utilisent plusieurs parties de leurs corps (articulateurs) simultanément, ce qui est difficile à capturer avec un système de notation écrite. Cette situation difficulté leur représentation dans de taches de Traitement Automatique du Langage Naturel (TALN). Pour ces raisons, le travail présenté dans ce document a comme objectif la construction d'une représentation abstraite de la LS; plus précisément, le but est de pouvoir représenter des collections de vidéo LS (corpus) de manière formelle. En générale, il s'agit de construire une couche de représentation intermédiaire, permettant de faire de la reconnaissance automatique indépendamment des technologies de suivi et des corpus utilisés pour la recherche. Cette couche corresponde à un système de transition d'états (STE), spécialement crée pour représenter la nature parallèle des LS. En plus, elle peut-être annoté avec de formules logiques pour son analyse, à travers de la vérification de modèles. Pour représenter les propriétés à vérifier, une logique multi-modale a été choisi : la Logique Propositionnelle Dynamique (PDL). Cette logique a été originalement crée pour la spécification de programmes. De manière plus précise, PDL permit d'utilise des opérateurs modales comme [a] et , représentant &lt;&gt; et &lt;&gt;, respectivement. Une variante particulaire a été développée pour les LS : la PDL pour Langue de Signes (PDLSL), qui est interprété sur des STE représentant des corpus. Avec PDLSL, chaque articulateur du corps (comme les mains et la tête) est vu comme un agent indépendant; cela veut dire que chacun a ses propres actions et propositions possibles, et qu'il peux les exécuter pour influencer une posture gestuelle. L'utilisation du framework proposé peut aider à diminuer deux problèmes importantes qui existent dans l'étude linguistique des LS : hétérogénéité des corpus et la manque des systèmes automatiques d'aide à l'annotation. De ce fait, un chercheur peut rendre exploitables des corpus existants en les transformant vers des STE. Finalement, la création de cet outil à permit l'implémentation d'un système d'annotation semi-automatique, basé sur les principes théoriques du formalisme. Globalement, le système reçoit des vidéos LS et les transforme dans un STE valide. Ensuite, un module fait de la vérification formelle sur le STE, en utilisant une base de données de formules crée par un expert en LS. Les formules représentent des propriétés lexicales à chercher dans le STE. Le produit de ce processus, est une annotation qui peut être corrigé par des utilisateurs humains, et qui est utilisable dans des domaines d'études tels que la linguistique<br>This thesis presents a formal framework for the representation of Signed Languages (SLs), the languages of Deaf communities, in semi-automatic recognition tasks. SLs are complex visio-gestural communication systems; by using corporal gestures, signers achieve the same level of expressivity held by sound-based languages like English or French. However, unlike these, SL morphemes correspond to complex sequences of highly specific body postures, interleaved with postural changes: during signing, signers use several parts of their body simultaneously in order to combinatorially build phonemes. This situation, paired with an extensive use of the three-dimensional space, make them difficult to represent with tools already existent in Natural Language Processing (NLP) of vocal languages. For this reason, the current work presents the development of a formal representation framework, intended to transform SL video repositories (corpus) into an intermediate representation layer, where automatic recognition algorithms can work under better conditions. The main idea is that corpora can be described with a specialized Labeled Transition System (LTS), which can then be annotated with logic formulae for its study. A multi-modal logic was chosen as the basis of the formal language: the Propositional Dynamic Logic (PDL). This logic was originally created to specify and prove properties on computer programs. In particular, PDL uses the modal operators [a] and to denote necessity and possibility, respectively. For SLs, a particular variant based on the original formalism was developed: the PDL for Sign Language (PDLSL). With the PDLSL, body articulators (like the hands or head) are interpreted as independent agents; each articulator has its own set of valid actions and propositions, and executes them without influence from the others. The simultaneous execution of different actions by several articulators yield distinct situations, which can be searched over an LTS with formulae, by using the semantic rules of the logic. Together, the use of PDLSL and the proposed specialized data structures could help curb some of the current problems in SL study; notably the heterogeneity of corpora and the lack of automatic annotation aids. On the same vein, this may not only increase the size of the available datasets, but even extend previous results to new corpora; the framework inserts an intermediate representation layer which can serve to model any corpus, regardless of its technical limitations. With this, annotations is possible by defining with formulae the characteristics to annotate. Afterwards, a formal verification algorithm may be able to find those features in corpora, as long as they are represented as consistent LTSs. Finally, the development of the formal framework led to the creation of a semi-automatic annotator based on the presented theoretical principles. Broadly, the system receives an untreated corpus video, converts it automatically into a valid LTS (by way of some predefined rules), and then verifies human-created PDLSL formulae over the LTS. The final product, is an automatically generated sub-lexical annotation, which can be later corrected by human annotators for their use in other areas such as linguistics

This thesis examines the use of expert systems in semi-formal domains. The research identifies the main problems with semi-formal domains and proposes and evaluates a number of different solutions to them. The thesis considers the traditional approach to developing expert systems, which sees domains as being formal, and notes that it continuously faces problems that result from informal features of the problem domain. To circumvent these difficulties experience or other subjective qualities are often used but they are not supported by the traditional approach to design. The thesis examines the formal approach and compares it with a semiformal approach to designing expert systems which is heavily influenced by the socio-technical view of information systems. From this basis it examines a number of problems that limit the construction and use of knowledge bases in semi-formal domains. These limitations arise from the nature of the problem being tackled, in particular problems of natural language communication and tacit knowledge and also from the character of computer technology and the role it plays. The thesis explores the possible mismatch between a human user and the machine and models the various types of confusion that arise. The thesis describes a number of practical solutions to overcome the problems identified. These solutions are implemented in an expert system shell (PESYS), developed as part of the research. The resulting solutions, based on non-linear documents and other software tools that open up the reasoning of the system, support users of expert systems in examining the boundaries of the knowledge base to help them avoid and overcome any confusion that has arisen. In this way users are encouraged to use their own skills and experiences in conjunction with an expert system to successfully exploit this technology in semi-formal domains.

A formal specification language used during the requirements phase can reduce errors and rework, but formal specifications are regarded as expensive to maintain, discouraging their adoption. This work presents a single-subject experiment that explores the costs of modifying specifications written in two different languages: a tabular notation, Software Cost Reduction (SCR), and a state-of-the-practice notation, Real-time Unified Modeling Language (UML). The study records the person-hours required to write each specification, the number of defects made during each specification effort, and the amount of time repairing these defects. Two different problems are specified&mdash;a Bidirectional Formatter (BDF), and a Bicycle Computer (BC)&mdash;to balance a learning effect from specifying the same problem twice with different specification languages. During the experiment, an updated feature for each problem is sent to the subject and each specification is modified to reflect the changes. <br /><br /> The results show that the cost to modify a specification are highly dependent on both the problem and the language used. There is no evidence that a tabular notation is easier to modify than a state-of-the-practice notation. <br /><br /> A side-effect of the experiment indicates there is a strong learning effect, independent of the language: in the BDF problem, the second time specifying the problem required more time, but resulted in a better-quality specification than the first time; in the BC problem, the second time specifying the problem required less time and resulted in the same quality specification as the first time. <br /><br /> This work demonstrates also that single-subject experiments can add important information to the growing body of empirical data about the use of formal requirements specifications in software development.

The government usually seeks help from private investors to be able to deliver public services. Private capital usually tends to concentrate on big profi table projects. In order to be able to carry out the smaller projects, an alternative to privatizations has to be proposed, in attention to the State’s inefficiency to deliver every service the society demands. In this article, the author proposes the civil society’s active participation as a way to carry out smaller projects efficiently. Nonetheless, civil participation is not possible without an attractive foment policy and the facilitation of particular initiatives given by the State. The article focuses particularly in the case of the Brazilian reality and other parts of LatinAmerica.<br>El Estado suele recurrir a la privatización para la implementación de servicios públicos. Generalmente, la inversión privada se concentra en grandes proyectos que le sean rentables. Se hace necesaria una alternativa al sistemade las privatizaciones, ya que el Estado tampoco puede asumir un rol activo en la prestación eficiente de todos los servicios que la sociedad demanda. En este artículo, el autor propone la participación activa de la sociedad civil para llevar acabo pequeños proyectos eficientemente. Sin embargo, ésta no es posible sin una correcta política de fomento y facilitación de iniciativas particulares por parte del Estado. Así, se pasa a analizar la situación de América Latina a la luz de la legislación y las experiencias internacionales.

Le développement de spécifications formelles correctes pour des systèmes et logiciels commence par l’analyse et la compréhension des besoins du client. Entre ces besoins décrits en langage naturel et leur spécification définie dans un langage formel précis, un écart existe et rend la tâche de développement de plus en plus difficile à accomplir. Nous sommes face à deux mondes distincts. Ce travail de thèse a pour objectif d’expliciter et d’établir des interactions entre ces deux mondes et de les faire évoluer en même temps. Par interaction, nous désignons les liens, les échanges et les activités se déroulant entre les différents documents. Parmi ces activités, nous présentons la validation comme un processus rigoureux qui démarre dès l’analyse des besoins et continue tout au long de l’élaboration de leur spécification formelle. Au fur et à mesure du développement, des choix sont effectués et les retours des outils de vérification et de validation permettent de détecter des lacunes aussi bien dans les besoins que dans la spécification. L’évolution des deux mondes est décrite via l’introduction d’un nouveau besoin dans un système existant et à travers l’application de patrons de développement. Ces patrons gèrent à la fois les besoins et la spécification formelle associée ; ils sont élaborés à partir de la description de la forme des besoins. Ils facilitent la tâche de développement et aident à éviter les risques d’oublis. Quel que soit le choix, des questions se posent tout au long du développement et permettent de déceler des lacunes, oublis ou ambiguïtés dans l’existant<br>The development of correct formal specifications for systems and software begins with the analysis and understanding of client requirements. Between these requirements described in natural language and their specification defined in a specific formal language, a gap exists and makes the task of development more and more difficult to accomplish. We are facing two different worlds. This thesis aims to clarify and establish interactions between these two worlds and to evolve them together. By interaction, we mean all the links, exchanges and activities taking place between the different documents. Among these activities, we present the validation as a rigorous process that starts from the requirements analysis and continues throughout the development of their formal specification. As development progresses, choices are made and feedbacks from verification and validation tools can detect shortcomings in requirements as well as in the specification. The evolution of the two worlds is described via the introduction of a new requirement into an existing system and through the application of development patterns. These patterns manage both the requirements and their associated formal specifications ; they are elaborated from the description of the form of the requirements in the client document. They facilitate the task of development and help to avoid the risk of oversights. Whatever the choice, the proposed approach is guided by questions accompanying the evolution of the whole system and makes it possible to detect imperfections, omissions or ambiguities in the existing

Le développement de spécifications formelles correctes pour des systèmes et logiciels commence par l’analyse et la compréhension des besoins du client. Entre ces besoins décrits en langage naturel et leur spécification définie dans un langage formel précis, un écart existe et rend la tâche de développement de plus en plus difficile à accomplir. Nous sommes face à deux mondes distincts. Ce travail de thèse a pour objectif d’expliciter et d’établir des interactions entre ces deux mondes et de les faire évoluer en même temps. Par interaction, nous désignons les liens, les échanges et les activités se déroulant entre les différents documents. Parmi ces activités, nous présentons la validation comme un processus rigoureux qui démarre dès l’analyse des besoins et continue tout au long de l’élaboration de leur spécification formelle. Au fur et à mesure du développement, des choix sont effectués et les retours des outils de vérification et de validation permettent de détecter des lacunes aussi bien dans les besoins que dans la spécification. L’évolution des deux mondes est décrite via l’introduction d’un nouveau besoin dans un système existant et à travers l’application de patrons de développement. Ces patrons gèrent à la fois les besoins et la spécification formelle associée ; ils sont élaborés à partir de la description de la forme des besoins. Ils facilitent la tâche de développement et aident à éviter les risques d’oublis. Quel que soit le choix, des questions se posent tout au long du développement et permettent de déceler des lacunes, oublis ou ambiguïtés dans l’existant<br>The development of correct formal specifications for systems and software begins with the analysis and understanding of client requirements. Between these requirements described in natural language and their specification defined in a specific formal language, a gap exists and makes the task of development more and more difficult to accomplish. We are facing two different worlds. This thesis aims to clarify and establish interactions between these two worlds and to evolve them together. By interaction, we mean all the links, exchanges and activities taking place between the different documents. Among these activities, we present the validation as a rigorous process that starts from the requirements analysis and continues throughout the development of their formal specification. As development progresses, choices are made and feedbacks from verification and validation tools can detect shortcomings in requirements as well as in the specification. The evolution of the two worlds is described via the introduction of a new requirement into an existing system and through the application of development patterns. These patterns manage both the requirements and their associated formal specifications ; they are elaborated from the description of the form of the requirements in the client document. They facilitate the task of development and help to avoid the risk of oversights. Whatever the choice, the proposed approach is guided by questions accompanying the evolution of the whole system and makes it possible to detect imperfections, omissions or ambiguities in the existing

Made available in DSpace on 2014-06-12T15:52:01Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2008<br>A integração de métodos formais com notações semi-formais visuais é uma tendência em engenharia de software. Métodos formais apresentam uma semântica precisa e permitem verificação de propriedades. No entanto, não são considerados intuitivos. Por outro lado, notações semi-formais visuais, como UML, são facilmente integradas no processo de desenvolvimento de software. Assim, métodos formais e semi-formais visuais são complementares. CSP e UML-RT são, respectivamente, exemplos de notação formal e diagramática usados para especificar e projetar sistemas concorrentes e distribuídos. CSP é um método formal no qual processos representam unidades comportamentais que se comunicam através de canais de comunicação, utilizando passagem de mensagem. UML-RT é uma extensão conservativa de UML na qual cápsulas são unidades comportamentais que se comunicam através de portas de comunicação. Portas realizam protocolos os quais especificam os sinais que podem ser enviados e recebidos através de uma porta, e a ordem na qual os sinais podem ser comunicados. Em um trabalho anterior, Ferreira apresentou um conjunto de regras que sistematizam o mapeamento de CSP para UML-RT, mas uma prova formal deste mapeamento não foi apresentada. Assim, para garantir consistência no desenvolvimento de sistemas concorrentes e distribuídos utilizando este mapeamento, a prova formal do mesmo é indispensável, uma vez que não faz sentido o esforço dedicado à especificação do sistema em CSP e a verificação de propriedades e refinamentos, se uma ou mais regras de mapeamento estiverem incorretas. No entanto, UMLRT não possui uma semântica formal padrão. Entre outras propostas de semântica formal, Ramos propõe uma semântica para UML-RT utilizando OhCircus (uma combinação de CSP e Z com características adicionais de orientação a objetos) como modelo semântico. Neste trabalho, é proposta uma variação da semântica de Ramos para UML-RT usando CSP como modelo semântico. Com base nesta semântica, é apresentada a prova do mapeamento de CSP para UML-RT, considerando o modelo de falhas e divergências de CSP. Assim, este trabalho consolida a integração de CSP e UML-RT proposta por Ferreira, no desenvolvimento de sistemas críticos, concorrentes e distribuídos. Um resultado interessante foi observar que, estritamente, as regras propostas por Ferreira não preservam a semântica de CSP, essencialmente com relação a aspectos de terminação dos processos

CertiCrypt est une bibliothèque qui permet de vérifier la sécurité exacte de primitives cryptographiques dans l'assistant à la preuve Coq. CertiCrypt instrumente l'approche des preuves par jeux, et repose sur de nombreux domaines comme les probabilités, la complexité, l'algèbre, la sémantique des langages de programmation, et les optimisations de programmes. Dans cette thèse, nous présentons deux exemples d'utilisation d'EasyCrypt: le schéma d'encryption Hashed ElGamal, et les protocoles à connaissance nulle. Ces exemples, ainsi que les travaux antérieurs sur CertiCrypt, démontrent qu'il est possible de formaliser des preuves complexes; toutefois, l'utilisation de CertiCrypt demande une bonne expertise en Coq, et demeure laborieuse. Afin de faciliter l'adoption des preuves formelles par la communauté cryptographique, nous avons développé EasyCrypt, un outil semi-automatique capable de reconstruire des preuves formelles de sécurité à partir d'une ébauche formelle de preuve. EasyCrypt utilise des outils de preuves automatiques pour vérifier les ébauches de preuves, puis les compiles vers des preuves vérifiables avec CertiCrypt. Nous validons EasyCrypt en prouvant à nouveau Hashed ElGamal, et comparons cette nouvelle preuve avec celle en CertiCrypt. Nous prouvons également le schéma d'encryption Cramer-Shoup. Enfin, nous expliquerons comment étendre le langage de CertiCrypt à des classes de complexité implicite, permettant de modéliser la notion de fonctions en temps polynomial.

Ce travail concerne les premières étapes du développement de logiciels et notamment l'activité de spécification. Il consiste en l'étude de deux formalismes : la méthode B et le langage UML. Il s'appuit sur la complémentarité de ces deux approches et contribue au rapprochement des langages formels et des notations graphiques à objets. Notre sujet de thèse vise à étudier et à mettre en oeuvre des techniques de construction qui permettent de faciliter le développement de spécifications formelles dans le langage B. Nous proposons pour cela d'utiliser l'ensemble des notations UML pour faciliter et documenter la spécification formelle. Le développement est fondé sur deux vues complémentaires : une vue UML qui décrit de manière synthétique et intuitive les différents aspects du futur systrème, une vue BG qui sert de support pour la vérification et permet l'étude rigoureuse des composants spécifiés. Notre modèle de développement est basé sur la construction initiale d'un modèle UML constitué de diagrammes de classes et de diagrammes d'états-transitions. Ce modèle est transformé à l'aide de schémas de dérivation ou une spécification formelle B qui sera complétée par la suite au niveau de la définition de ses opérations et/ou par des contraintes qui ne figurent pas dans les diagrammes UML. La conception des modèles peut être facilitée par l'utilisation de patterns largement répandus au niveau du développement par objets. Nous fournissons ainsi une démarche qui permet l'utilisation de patterns pour la spécification conjointe en B et en UML. Finalement, nous proposons de générer et de prouver des obligations de preuves complémentaires à la méthode B. Le rôle de celles-ci est de vérifier des contraintes liées à l'utilisation des objets<br>This work concerns the first stages of the development of software in particular the activity of specification. He(it) consists of the study of two formalisms: the method B and the language UML. He(it) appuit on the complementarity of these two approaches and contributes to the link(merger) of the formal languages and the graphic notations with objects. Our thesis subject aims at studying and at implementing(operating) techniques of construction which allow to facilitate the development of formal specifications in the language B. We suggest for it using all the notations UML to facilitate and document the formal specification. The development is based(established) on two complementary(additional) views(sights) : A view(sight) UML which describes in a synthetic and intuitive way the various aspects of future systrème, a view(sight) BG which serves as support(medium) for the check and allows the rigorous study of the specified components. Our model of development is based on the initial construction of a model UML established(constituted) by diagrams of classes and by diagrams of states-transition. This model is transformed by means of plans of diversion or a formal specification B which will be afterward completed at the level of the definition of its operations and/or by constraints which do not appear in diagrams UML. The conception(design) of the models can be facilitated by the use of patterns widely spread at the level of the development by objects. Finally, we suggest generating and proving obligations of complementary proofs to the method B. The role of these is to verify constraints bound to the use of objects

Dependent type theories are a kind of mathematical foundations investigated both for the formalisation of mathematics and for reasoning about programs. They are implemented as the kernel of many proof assistants and programming languages with proofs (Coq, Agda, Idris, Dedukti, Matita, etc). Dependent types allow to encode elegantly and constructively the universal and existential quantifications of higher-order logics and are therefore adapted for writing logical propositions and proofs. However, their usage is not limited to the area of pure logic. Indeed, some recent work has shown that they can also be powerful for driving the construction of programs. Using more precise types not only helps to gain confidence about the program built, but it can also help its construction, giving rise to a new style of programming called Type-Driven Development. However, one difficulty with reasoning and programming with dependent types is that proof obligations arise naturally once programs become even moderately sized. For example, implementing an adder for binary numbers indexed over their natural number equivalents naturally leads to proof obligations for equalities of expressions over natural numbers. The need for these equality proofs comes, in intensional type theories (like CIC and ML) from the fact that in a non-empty context, the propositional equality allows us to prove as equal (with the induction principles) terms that are not judgementally equal, which implies that the typechecker can't always obtain equality proofs by reduction. As far as possible, we would like to solve such proof obligations automatically, and we absolutely need it if we want dependent types to be use more broadly, and perhaps one day to become the standard in functional programming. In this thesis, we show one way to automate these proofs by reflection in the dependently typed programming language Idris. However, the method that we follow is independent from the language being used, and this work could be reproduced in any dependently-typed language. We present an original type-safe reflection mechanism, where reflected terms are indexed by the original Idris expression that they represent, and show how it allows us to easily construct and manipulate proofs. We build a hierarchy of correct-by-construction tactics for proving equivalences in semi-groups, monoids, commutative monoids, groups, commutative groups, semi-rings and rings. We also show how each tactic reuses those from simpler structures, thus avoiding duplication of code and proofs. Finally, and as a conclusion, we discuss the trust we can have in such machine-checked proofs.

Students who identify as being from an ethnic minority are under-represented within school geography in England at Key Stage 4 (ages 14 – 16) and Key Stage 5 (ages 16 – 18). At these stages geography is an optional subject and how students view geographical knowledge may influence their GCSE and A level subject choices. This study uses an intersectional theoretical lens to explore representations of geographical knowledge by students of different ethnicities, the stories that relate to these representations and how the students accounted for the GCSE and A level subject choices that they made. The first part of the study reveals a lack of empirical and contemporary research into ethnic minority students’ views of geographical knowledge and subject choices. This is followed by a two-strand exploratory case study at one girls’ grammar school in England. The practitioner-researcher strand was two phase; in the first phase, 314 sixth form students (aged 16 – 18) completed a questionnaire to gauge initial views of geographical knowledge. During the second phase, eight of these students represented their views of geographical knowledge through collages, critical incident charts and semi-structured interviews that explored their stories in depth. In parallel, a group of Year 10 (aged 14 – 15) students as researchers used questionnaires to investigate the influence of parents and other factors contributing to students’ subject choices at GCSE level. In the study, geographical knowledge was represented in different ways given different methods. It was found to be diverse and individual, although it was possible for specific themes to be identified. The representations reflected the characteristics and concepts from students’ recent formal experiences of geography. Informal experiences also featured but these were not always explicit or straightforwardly definable. Unless students could see the intrinsic usefulness of their view of geographical knowledge then they were unlikely to choose the subject past GCSE level. This study expands theoretical conceptualisations of how students represent geographical knowledge and the factors affecting subject choice, engages students as researchers in a methodologically innovative way and provides a rich and detailed account of post-14 subject choice by ethnic minority students which otherwise does not exist in an English context.

I denna kandidatuppsats undersöks uppfattningen av översatta texter hos en grupp med italienska som förstaspråk i syfte att redovisa om ett preferensmönster finns gällande tilltal, idiomatiska uttryck, meningsbyggnad och meningslängd. Texter som är undersökningens material i denna studie översätts enligt Nidas principer om formell och dynamisk ekvivalens och definieras enligt Tourys teorier. Undersökningen genomförs genom ett antal öppna frågor som ställs till respondenterna under semistrukturerade intervjuer. Slutsatserna dras från diskussionen av respondenternas svar kopplad till teorin samt redovisning av resultat för preferensmönstret. Studien visar att kontext, forum och målgruppen är avgörande för valet av översättningsstrategin.Förslag på vidare forskning ges i det slutliga kapitlet med formulering av hypotes gällande behovet att bestämma översättningsstrategi och tillämpning av normer enligt texttyp och målgrupp.<br>This bachelor’s thesis is a study of perception of translated texts in a group of people with Italian as their first language. The aim of this work is to investigate whether a pattern in the preference of form of address, idiomatic expressions and syntax can be identified. The texts that are used in this study are translated according to Nida’s principles of formal and dynamic equivalence and are defined according to Toury’s theories.The study is conducted thanks to a set of open questions asked to the responders in semi-structured interviews. The conclusions are derived from the analysis of the responders’ answers in relation to the theories mentioned and the pattern of preferences revealed. The study shows that context, forum and target group are crucial for the choice of which translation strategy it will be used,Finally, we outline a proposal for further research to test the hypothesis that translation strategies and application of norms should be chosen according to the type of text and the target group.Nyckelord

The growing need for computer software in different sectors of activity, (health, agriculture, industries, education, aeronautic, science and telecommunication) together with the increasing reliance of the society as a whole on information technology, is placing a heavy and fast growing demand on complex and high quality software systems. In this regard, the anticipation has been on non-functional requirements (NFRs) engineering and formal methods. Despite their common objective, these techniques have in most cases evolved separately. NFRs engineering proceeds firstly, by deriving measures to evaluate the quality of the constructed software (product-oriented approach), and secondarily by improving the engineering process (process-oriented approach). With the ability to combine the analysis of both functional and non-functional requirements, Goal-Oriented Requirements Engineering (GORE) approaches have become de facto leading requirements engineering methods. They propose through refinement/operationalisation, means to satisfy NFRs encoded in softgoals at an early phase of software development. On the other side, formal methods have kept, so far, their promise to eliminate errors in software artefacts to produce high quality software products and are therefore particularly solicited for safety and mission critical systems for which a single error may cause great loss including human life. This thesis introduces the concept of Complementary Non-functional action (CNF-action) to extend the analysis and development of NFRs beyond the traditional goals/softgoals analysis, based on refinement/operationalisation, and to propagate the influence of NFRs to other software construction phases. Mechanisms are also developed to integrate the formal technique Z/Object-Z into the standardised User Requirements Notation (URN) to formalise GRL models describing functional and non-functional requirements, to propagate CNF-actions of the formalised NFRs to UCMs maps, to facilitate URN construction process and the quality of URN models.<br>School of Computing<br>D. Phil (Computer Science)

碩士<br>國立臺灣大學<br>電子工程學研究所<br>106<br>Engineering change order (ECO) is a popular technique for rectifying design errors and specification changes in late design stages. We present a two-phase semi-formal patch generation to rectify multiple errors. We first 1) discover the functional matches in two circuits, then 2) optimize and generate a patch circuit from the matches. The ECO engine in this thesis discovers functional and structural matches in two circuits by the FRAIG technique and the simulation-guided cut-matching algorithm. Then, the combinational equivalence checking technique combined with a linear-time selection heuristic is processed to minimize the patch size from the matches. The experimental results show that this ECO engine can rectify circuits with small patch size within reasonable runtime.

Specification plays a vital role in software engineering to facilitate the development of highly dependable software. The importance of specification in software development is to serve, amongst others, as a communication tool for stakeholders in the software project. The specification also adds to the understanding of operations, and describes the properties of a system. Various techniques may be used for specification work. Z is a formal specification language that is based on a strongly-typed fragment of Zermelo-Fraenkel set theory and first-order logic to provide for precise and unambiguous specifications. Z uses mathematical notation to build abstract data, which is necessary for a specification. The role of abstraction is to describe what the system does without prescribing how it should be done. Diagrams, on the other hand, have also been used in various areas, and in software engineering they could be used to add a visual component to software specifications. It is plausible that diagrams may also be used to reason in a semi-formal way about the properties of a specification. Many diagrammatic languages are based on contours and set theory. Examples of these languages are Euler-, Spider-, Venn- and Pierce diagrams. Euler diagrams form the foundation of most diagrams that are based on closed curves. Diagrams, on the other hand, have also been used in various areas, and in software engineering they could be used to add a visual component to software specifications. It is plausible that diagrams may also be used to reason in a semi-formal way about the properties of a specification. Many diagrammatic languages are based on contours and set theory. Examples of these languages are Euler-, Spider-, Venn- and Pierce diagrams. Euler diagrams form the foundation of most diagrams that are based on closed curves. The purpose of this research is to demonstrate the extent to which diagrams can be used to represent a Z specification. A case study is used to transform the specification modelled with Z language into a diagrammatic specification. Euler, spider, Venn and Pierce diagrams are combined for this purpose, to form one diagrammatic notation that is used to transform a Z specification<br>School of Computing<br>M. Sc. (Information Systems)

碩士<br>國立中正大學<br>資訊工程研究所<br>91<br>A major goal in hardware design is to guarantee that a design module conforms to its requirement specifications such as functionality demands. Therefore, verification plays an important role in the design process. With rapid technology progress in deep submicron design and the advent of System-on-Chip (SoC), functional verification has become a major bottleneck in system design. In general, functional simulation and formal verification are the two most general verification methods which are extensively used in the industry and have become topics for research in the academia. While functional simulation and formal verification have their distinctive features and benefits in verifying the correctness of an early design, each of them has their own limitations at the system level of verification. Therefore, an alternative methodology, called semi-formal verification, which is the combined application of formal verification technology and simulation technology, has been recently proposed. We have proposed a novel semi-formal verification framework which is applied, when a Testbench is not passed during a simulation process, in order to analysis the bugs easily and to ensure to eliminate the design error entirely. Whenever a test case consisting of stimulus inputs and expected outputs fails, a simulation error trace is detected. Our methodology then tries to generate a formal property from the error trace, which can be need in model checker to eliminate an related error that conform to the property. This verification flow allows us to overcome two drawbacks: (1) simulation can only find error and not prove the absence of error; and (2) model checking has the famous state space explosion problem. On modifying a buggy design and re-simulation of the corrected design, a designer can be sure if the single instance of design error is eliminated, whereas using our approach the designer can be sure that all related errors are eliminated, which also proves the absence of that kind of error. We have solved several issues encountered in our methodology. Firstly, we need to generate a precise verification model from RTL descriptions in HDL. Secondly, we need to overcome the limitations of modeling hardware behaviors in the SGM model checker. Finally, we need a procedure to generate formal properties from simulation error traces and Testbench. Through verification of two Verilog design examples, we illustrate the architecture and benefits of our proposed verification framework. Further, we also demonstrate how related design errors are found in our approach.

The derivation of a specification document that is understandable, precise and unambiguous is indispensable to successful software development. This work investigates the advantages and disadvantages of four different specification approaches which vary in their degree of formality. The thesis outlines qualities of a good specification. An example requirements specification of a case study system is produced using each technique. The four specification approaches are ad hoc natural language approach (informal), threadsbased technique (structured informal), Computer-Aided Software Engineering (CASE) methodology Structured Analysis (semi-formal), and the mathematical notation Z (formal). The specification techniques are compared based on their likelihood to produce a specification document which is useful to customers, design engineers, test engineers, and maintenance personnel. The main conclusion is that using techniques that provide both a high degree of guidance and process description for deriving the specification is critical to achieve high quality specifications. Hence, a good specification technique must inherently have guidelines that facilitate the specification of requirements in an understandable, precise and unambiguous manner.

The verification of analog designs has been a challenging task for a few years now. Several approaches have been taken to tackle the main problem related to the complexity that such task presents to design and verification teams. The methodology presented in this document is based on the experiences and research work carried out by the Concordia University's Hardware Verification and the U. of Texas' IC systems design groups. The representation of complex systems where different interactions either mechanical or electrical take place requires an intricate set of mathematical descriptions which greatly vary according to the system under test. As a simple and very relevant example one can look at the integration of RF-MEMS as active elements in System-On-Chip architectures. In order to tackle such heterogeneous interaction for a consistent model, the use of stochastic hybrid models is described and implemented for very simple examples using high level modeling tools for a succinct and precise description.<br>text

This study examines the current pastoralists' education situation in Uganda in the context of the education policy established, and non-formal education interventions being conducted among the Bahima and Karimojong pastroralists by both Governmental and Non-Governmental Organizations, as an attempt to address the problems and issues of illiteracy and pastoral development. It is evident that education for pastoralists in Uganda creates a social consciousness with values, norms, knowledge and skills, which have a complex and dynamic relationship among the pastoralists. The problems of investigation in this research focus on information available on the functioning of pastoralism for effective provision of non-formal education programmes to the Bahima and Karimojong pastoralists; and how effectively the providers of non-formal education programmes can integrate the nomadic livelihood in the provision of non-formal education The literature review has focused on the Bahima and Karimojong pastoralists, but attempts have also been made to draw relevant lessons from other nomadic groups like Gypsies, travellers, and occupational travellers. The review has been intended to sharpen specific aspects related to pastoral and national education practices that can enable appropriate and strategic provision and implementation of non-formal education programmes to occur among the Bahima and Karimojong pastoralists in their pastoral context. Qualitative research methods used in the study were fundamentally relevant and suited for locating the meaning that semi-nomadic Bahima and Karimojong pastoralists placed on events, processes and structures of their lives, their perceptions, assumptions, prejudgments, presumptions, and for connecting these meanings to the social world around them. Presentation and analysis of data is divided into three sections including a recast of the items in the interview schedules, a summary of the research findings presented on a conceptually clustered Matrix Sheet, and a presentation of the data analysis resulting form the data displayed on the Matrix Sheet. Recommendations of the study have been clustered under the following three thematic categories: · Relevance of non-formal education programmes to the Bahima and Karimojong pastoraslist, · Factors for implementation of non-formal education programmes, and · Strategies for implementation and sustenance of non-formal education programmes among the Bahima and Karimojong pastoralists.<br>Educational Studies<br>MED (COMPARATIVE EDUCATION)

The way in which application systems and software are built has changed dramatically over the past few years. This is mainly due to advances in hardware technology, programming languages, as well as the requirement to build better software application systems in less time. The importance of mondial (worldwide) communication between systems is also growing exponentially. People are using network-based applications daily, communicating not only locally, but also globally. The Internet, the global network, therefore plays a significant role in the development of new software. Distributed object computing is one of the computing paradigms that promise to solve the need to develop clienVserver application systems, communicating over heterogeneous environments. This study, of limited scope, concentrates on one crucial element without which distributed object computing cannot be implemented. This element is the communication software, also called middleware, which allows objects situated on different hardware platforms to communicate over a network. Two of the most important middleware standards for distributed object computing today are the Common Object Request Broker Architecture (CORBA) from the Object Management Group, and the Distributed Component Object Model (DCOM) from Microsoft Corporation. Each of these standards is implemented in commercially available products, allowing distributed objects to communicate over heterogeneous networks. In studying each of the middleware standards, a formal way of comparing CORBA and DCOM is presented, namely meta-modelling. For each of these two distributed object infrastructures (middleware), meta-models are constructed. Based on this uniform and unbiased approach, a comparison of the two distributed object infrastructures is then performed. The results are given as a set of tables in which the differences and similarities of each distributed object infrastructure are exhibited. By adopting this approach, errors caused by misunderstanding or misinterpretation are minimised. Consequently, an accurate and unbiased comparison between CORBA and DCOM is made possible, which constitutes the main aim of this dissertation.<br>Computing<br>M. Sc. (Computer Science)

This thesis presents a JML-based strategy that incorporates formal specifications into the software development process of object-oriented programs. The strategy evolves functional requirements into a “semi-formal” requirements form, and then expressing them as JML formal specifications. The strategy is implemented as a formal-specification pseudo-phase that runs in parallel with the other phase of software development. What makes our strategy different from other software development strategies used in literature is the particular use of JML specifications we make all along the way from requirements to validation-and-verification.<br>Orientador: Néstor Cataño

Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2021.<br>Este trabajo consiste en el diseño e implementación de un lenguaje de programación estructurado basado en el lenguaje Pascal, orientado al aprendizaje de algoritmos y estructura de datos. El mismo es utilizado actualmente en una materia de la FaMAF, contando con una definición informal. Existe una sintaxis concreta relativamente consolidada aunque no especificada, y la semántica está definida de manera intuitiva. En el trabajo se estudió la información disponible a partir del dictado de la materia obteniendo una definición formal de la sintaxis abstracta, en conjunto con la definición de varios chequeos estáticos, como el sistema de tipos.<br>This work consists of the design and implementation of a structured programming language based on the Pascal language, oriented to the learning of algorithms and data structure. It is currently used in a FaMAF subject, with an informal definition. There is a relatively well established but unspecified concrete syntax, and the semantics are intuitively defined. In the work, the information available from the dictation of the subject was studied, obtaining a formal definition of the abstract syntax, together with the definition of several static checks, such as the type system.<br>Fil: Gobbi, Matías Federico. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina.

The thesis is interested in the problem of musical sign. In which ways can we speak about musical sign and which elements of musical material can become signs? These are the basic questions which we are interested in. This thesis is divided into three parts. The first part attends to the common theory of sign. The historical survey with the main ideas of philosophers and thinkers will be helpful to find out basic terms and problems of semiotics. In the second part of thesis we look at the historical reflection of musical sign in order to find out in which way it was treated with music and musical sign in each historical period of European music. In the third part we focus on musical semiotics, but we will consider some problems of musical aesthetics and musical psychology, too. In the end we make recapitulation of answers to the aforesaid questions.

This study investigates the possibility of applying Hatten’s theory of musical gesture to a formal system of musical analysis. Using historical antecedents and established musicological practice as a guide, a range of musical parameters in a motive length span of music are incorporated into a single gesture. This gesture forms the basic semantic unit upon which an analytical tableau structure is built, and a syntax is developed to allow derivations of new gestures; a large scale structure displaying fractal-like self-similarity is then proposed. The completed system is applied to the analysis of the ‘Adagio’ of Mozart’s Flute Quartet K.285 to test whether it can consistently be implemented and whether it produces falsifiable results while maintaining predictive power. It is found that these requirements are indeed met and that a set of inference rules can be derived suggesting that the proposed system has ample scope for further development.<br>Art History, Visual Arts & Musicology<br>M. Mus.

This research investigates the role business incubators on the MSMEs’ access to informal and semi-formal finance. To meet this purpose, firstly, the relationship between business incubation models and models of financial accessibility is assessed. secondly, the contribution of business incubators to the MSMEs informal and semi-formal financial accessibility is determined, by assessing the direct impact of monitoring services on financial accessibility and also assessing the incubator’s financial intermediation role between incubatees and financiers. Due to the important role played by social capital in non-formal financing, the influence of both incubatee and incubator manager’s social capital on incubatee’s informal and semi-formal financial accessibility is also investigated. The results indicate that, business incubator’s monitoring services have significant positive influence on incubatee’s access to informal and semi-formal finance, and also there is a significant positive relationship between monitoring services and financial management capabilities. Also, incubatee’s financial management capabilities have significant positive impact on semi-formal financial accessibility, nevertheless, there is insignificant relationship between incubatee’s financial management capabilities and informal financial accessibility. Furthermore, the results show, incubatee’s bonding and bridging social capital have direct positive impact on both informal and semi-formal financial accessibility, while incubator manager’s linking social capital has positive impact on semi-formal financial accessibility but insignificant impact on informal financial accessibility. Incubatee’s bridging social capital also negatively moderates the relationship between financial management capabilities and semi-formal financial accessibility, whereas incubatee’s bonding has no moderating effect on the same relationship. Incubator manager’s bonding and bridging social capital and incubatee’s linking social capital have insignificant direct impact on both informal and semi-formal financial accessibility, as well as insignificant moderating impact on the relationship between financial management capabilities and semi-formal financial accessibility. These findings show the importance of financial management capabilities on incubatee’s access to semi-formal finance and highlights the role of incubatee’s bonding and bridging network links and incubator manager’s linking social networks to the incubatee’s access to non-formal finance. They also reveal that informal financiers do not consider incubatee’s financial management capabilities as an important criterion in deciding to provide them credits:Acknowledgement i Table of contents iii List of tables viii List of figures xii Abbreviations xv Zusammenfassung xx Summary xxxii CHAPTER ONE 1 INTRODUCTION 1 1.1 Background to the problem 1 1.2 Statement of the Problem 4 1.3 Objectives of the study 10 1.3.1 General objective 10 1.3.2 Specific objectives 10 CHAPTER TWO 11 LITERATURE REVIEW 11 2.1 Start-ups and Micro, Small and Medium Enterprises 11 2.1.1 Micro, Small and Medium Enterprises 11 2.1.1.1 MSMEs’ sector in Tanzania 14 2.1.2 Start-ups 15 2.1.2.1 Startups in Tanzania 16 2.2 Business incubators 18 2.2.1 Services provided by business incubators 21 2.2.2 Business incubators in Tanzania 23 2.3 Financial management capabilities 28 2.3.1 Financial management capabilities in MSMEs 29 2.4 Financial system 32 2.4.1 Formal financing 33 2.4.2 Informal financing 33 2.4.3 Semi-formal financing 34 2.4.4 Financing system in Tanzania 34 2.4.5 Informal and Semi-formal financing system in Tanzania 36 2.4.5.1 Informal financiers 37 2.4.5.2 Semi-formal financiers 45 2.5 MSMEs’ financial accessibility 52 2.5.1 MSMEs’ financial accessibility in Tanzania 55 2.5.2 The role of business incubators in promoting MSMEs’ access to finance 56 2.6 Information asymmetries between MSMEs and financiers 59 2.7 Theory of financial intermediation 61 2.8 Social capital 62 2.8.1 Role of social capital on MSMEs’ access to finance 65 2.9 Summary of the theoretical framework 69 2.10 Proposed model 70 CHAPTER THREE 75 RESEARCH METHODOLOGY 75 3.1 Research Design 75 3.2 Study Area 76 3.3 Targeted population 78 3.4 Sample 79 3.5 Operational definitions and measurement of the variables 83 3.5.1 Variable indicators 83 3.5.2 Business incubators' monitoring services 83 3.5.3 Financial management capabilities 84 3.5.4 Incubatee's bonding social capital 84 3.5.5 Incubatee's bridging social capital 85 3.5.6 Incubatee's linking social capital 85 3.5.7 Incubator manager's bonding social capital 86 3.5.8 Incubator manager's bridging social capital 86 3.5.9 Incubator manager's linking social capital 87 3.5.10 MSMEs’ Financial accessibility 87 3.6 Data collection instrument 92 3.6.1 Questionnaire 92 3.6.2 Personal interviews 93 3.7 Data collection 93 3.8 Data Analysis 94 3.8.1 Qualitative data analysis 94 3.8.2 Quantitative analysis 95 3.8.2.1 Data preparation 95 3.8.2.2 Descriptive statistics 96 3.8.2.3 Factor analysis 96 3.8.2.4 Inferential Statistics 104 3.8.2.4.1 Spearman correlations analysis 105 3.8.2.4.2 Kruskal-Wallis test 105 3.8.2.4.3 Partial Least Squares regressions analysis 105 3.9 Validity and Reliability 106 3.9.1 Validity and reliability of qualitative research 106 3.9.2 Validity and reliability in quantitative research 107 CHAPTER FOUR 110 PRESENTATION OF FINDINGS 110 4.1 Introduction 110 4.2 Qualitative results 110 4.2.1 Current status of business incubation programs in Tanzania 110 4.2.2 Factors for business incubators’ successful financial intermediary role118 4.3 Quantitative results 132 4.3.1 Descriptive results 132 4.3.1.1 Sample demography 133 4.3.1.1.1 Relationship between age and incubation period of incubated MSMEs 133 4.3.1.1.2 Categorizing incubated MSMEs by number of employees and business capital 135 4.3.1.1.3 Distribution of incubatees by their nature of ownership and business activity 138 4.3.1.1.4 Financiers’ provision of requested amount of loans to incubatees 140 4.3.1.2 The contribution of business incubators to MSMEs financial accessibility 145 4.3.1.2.1 The Business Incubator's Monitoring services 146 4.3.1.2.2 Financial Management capabilities of incubatees 147 4.3.1.2.3 MSMEs’ financial accessibility 149 4.3.1.3 Relationship between business incubation models and models of MSMEs financing 150 4.3.1.4 Factors for successful intermediary role of an incubator 152 4.3.1.5 Incubatees and incubator managers’ social capital on Incubatees' financial accessibility 155 4.3.2 The impact of business incubation on MSMEs access to informal and semi-formal finance 160 4.3.2.1 Demographic characteristics of incubated enterprises 161 4.3.2.2 Relationship between business incubation models and models of financial accessibility 165 4.3.2.3 Contribution of incubators to the MSMEs informal and semi-formal financial accessibility 166 4.3.2.3.1 Impact of business incubator’s monitoring services on MSMEs’ informal and semi-formal financial accessibility 167 4.3.2.3.2 Business incubators’ financial intermediation role between incubated MSMEs and financiers. 170 4.3.2.4 Impact of incubatee and incubator manager’s social capital on iMFA and sMFA 173 4.3.2.5 Moderating impact of Incubatee's and incubator manager's social capital on the FMC-MFA relationship 179 4.4 Summary of chapter four 183 4.4.1 Developing a model on incubated MSMEs’ access to informal and semi- formal finance. 190 4.4.1.1 A model on incubated MSMEs’ access to informal finance 190 4.4.1.2 A model on incubated MSMEs’ access to semi-formal finance. 191 4.4.1.3 The influence of demographic characters on the relationship between social capital and financial accessibility. 192 CHAPTER FIVE 196 DISCUSSION OF FINDINGS 196 5.1 Introduction 196 5.2 Demographic characteristics of incubatees 196 5.3 Relationship between business incubation models and models of financial accessibility 201 5.4 Business incubators’ financial intermediation role between MSMEs and financiers. 203 5.5 Factors for successful business incubator’s financial intermediary role 207 5.6 Impact of incubatee’s and incubator manager’s social capital on informal and semi-formal financial accessibility 209 5.7 Moderating impact of Incubatee's and incubator manager's social capital on the FMC-MFA relationship 212 CHAPTER SIX 214 CONCLUSIONS AND RECOMMENDATIONS 214 6.1 Conclusions 214 6.2 Recommendations 221 6.3 Scope for further research 229 Reference 234 Appendix I Total Variance Explained 253 Appendix II Component Matrix 254 Appendix III Pattern Matrix 255 Appendix IV Questionnaire 256 Appendix V Questionnaire (Swahili version) 261 Appendix VI Interview guide for the financiers (English version) 266 Appendix VII Interview guide for the financiers (Swahili version) 267 Apendix VIII Interview guide for incubators’ managers and key informants (English version) 268 Appendix IX Interview guide for incubators’ managers and key informants (Swahili version) 269 Appendix X Eigenständigkeitserklärung 270

Formal specification of software systems has been very promising. Critics against the end results of formal methods, that is, producing quality software products, is certainly rare. Instead, reasons have been formulated to justify why the adoption of the technique in industry remains limited. Some of the reasons are: • Steap learning curve; formal techniques are said to be hard to use. • Lack of a step-by-step construction mechanism and poor guidance. • Difficulty to integrate the technique into the existing software processes. Z is, arguably, one of the successful formal specification techniques that was extended to Object-Z to accommodate object-orientation. The Z notation is based on first-order logic and a strongly typed fragment of Zermelo-Fraenkel set theory. Some attempts have been made to couple Z with semi-formal notations such as UML. However, the case of coupling Object-Z (and also Z) and the Use Case Maps (UCMs) notation is still to be explored. A Use Case Map (UCM) is a scenario-based visual notation facilitating the requirements definition of complex systems. A UCM may be generated either from a set of informal requirements, or from use cases normally expressed in natural language. UCMs have the potential to bring more clarity into the functional description of a system. It may furthermore eliminate possible errors in the user requirements. But UCMs are not suitable to reason formally about system behaviour. In this dissertation, we aim to demonstrate that a UCM can be transformed into Z and Object-Z, by providing a transformation framework. Through a case study, the impact of using UCM as an intermediate step in the process of producing a Z and Object-Z specification is explored. The aim is to improve on the constructivity of Z and Object-Z, provide more guidance, and address the issue of integrating them into the existing Software Requirements engineering process.<br>Computer Science<br>M. Sc. (Computer Science)