Thesis (M. Tech.) - Central University of Technology, Free State, 2007

The main part in the testing of the software is in the generation of test cases suitable for software system testing. The quality of the test cases plays a major role in reducing the time of software system testing and subsequently reduces the cost. The test cases, in model de- sign stages, are used to detect the faults before implementing it. This early detection offers more flexibility to correct the faults in early stages rather than latter ones. The best of these tests, that covers both static and dynamic software system model specifications, is one of the chal- lenges in the software testing. The static and dynamic specifications could be represented efficiently by Unified Modelling Language (UML) class diagram and sequence diagram. The work in this thesis shows that High Level Petri Nets (HLPN) can represent both of them in one model. Using a proper model in the representation of the software specifications is essential to generate proper test cases. The research presented in this thesis introduces novel and automated test cases generation techniques that can be used within a software sys- tem design testing. Furthermore, this research introduces e cient au- tomated technique to generate a formal software system model (HLPN) from semi-formal models (UML diagrams). The work in this thesis con- sists of four stages: (1) generating test cases from class diagram and Object Constraint Language (OCL) that can be used for testing the software system static specifications (the structure) (2) combining class diagram, sequence diagram and OCL to generate test cases able to cover both static and dynamic specifications (3) generating HLPN automat- ically from single or multi sequence diagrams (4) generating test cases from HLPN. The test cases that are generated in this work covered the structural and behavioural of the software system model. In first two phases of this work, the class diagram and sequence diagram are decomposed to nodes (edges) which are linked by Classes Hierarchy Table (CHu) and Edges Relationships Table (ERT) as well. The linking process based on the classes and edges relationships. The relationships of the software system components have been controlled by consistency checking technique, and the detection of these relationships has been automated. The test cases were generated based on these interrelationships. These test cases have been reduced to a minimum number and the best test case has been selected in every stage. The degree of similarity between test cases is used to ignore the similar test cases in order to avoid the redundancy. The transformation from UML sequence diagram (s) to HLPN facilitates the simpli cation of software system model and introduces formal model rather than semi-formal one. After decomposing the sequence diagram to Combined Fragments, the proposed technique converts each Combined Fragment to the corresponding block in HLPN. These blocks are con- nected together in Combined Fragments Net (CFN) to construct the the HLPN model. The experimentations with the proposed techniques show the effectiveness of these techniques in covering most of the software system specifications.

QC 351 A7 no. 16 / This document has been prepared to form the basis for the operational specifications for the Cassegrain instrumentation for the 90-inch telescope of the Steward Observatory. The publication of this document is for the purpose of providing guidance to other astronomical groups who may have use for the considerations recorded herein.

The aim of this thesis is to illustrate the problems of auditing of information technology and to propose a design of an information system which would support the audit process. The scope of such system is beyond the framework of this thesis and therefore the specification of requirements and system design is only on a general level. We will approach in a more detailed way only one selected component, which is to be implemented. This tool is concerned with the management of assignments. It will record and evaluate the assignments, including the hours charged and hours budgeted to an assignment. In this paper, the system is described, analyzed in detail with respect to the requirements, then implemented, and its functionality tested.

Un Système de production peut être représenté par les systèmes à événements discrets. En dehors de la planification (où les gens travaillent avec des ratios de produits fabriqués par semaine ou par jour), la modélisation pourrait être basée sur les concepts d'événement et d'activités. Un événement correspond à un changement d'état. Une activité est une boîte noire d'encapsulation de ce qui se passe entre deux événements. En utilisant les réseaux de Petri (RdP), les événements sont représentés par les transitions, et les activités par les lieux. Notre travail propose une synthèse de commande par supervision pour les systèmes d'événements discrets modélisés par une classe de réseaux de Petri appelé graphe d'événements. L'objective de cette thèse est de concevoir un superviseur capable d'aider à améliorer la performance de système et de protéger le système en respectant des spécifications données par le fabricant ou le client selon les besoins et les conditions de travail. Pour modéliser ces spécifications, nous avons proposé un nouveau modèle mathématique de contrainte, appelé Contrainte d'Exclusion de Marquage (CEM). La deuxième contribution principale de ma thèse est de synthétiser une technique efficace et simple pour construire un superviseur qui impose le système de respecter des contraintes en évitant l'ensemble des états interdits modélisé par CEM. Nous avons également développé cette synthèse pour résoudre le problème d'existence des événements incontrôlables et des événements inobservables. Parfois, afin d'étudier les aspects liés à la performance, nous devons prendre le temps en considération. Donc, nous avons résolu aussi le problème des événements temporisé en utilisant RdP temporisés soumis à CEM / A manufacturing system may be represented by Discrete Event System (DES). Apart from planning (where people work with ratios of products fabricated per week or per day), any modelling could be based on the concepts of event and activities. An event corresponds to a state change. An activity is a black-box summarizing what is occurring between two events. When using Petri Nets, events are associated with transitions, and activities with places. Our work proposes a supervisory synthesis for Discrete Event System modelled by a class of Petri Net called Marked Graph. The objective of this synthesis is to build a control law that enforces the system to respect a set of given specifications. To model these specifications, we propose new mathematical formulas called Marking Exclusion Constraint (MEC). This model is our first contribution. The Second main contribution of my thesis is to synthesize a computationally efficient technique to build a supervisor that enforces the system to respect the constraints by avoiding a set of forbidden states modelled by MEC specifications. We extend this synthesis technique to solve the problem in the presence of uncontrollable events and unobservable events. Sometimes in order to study the performance aspects, we must take in consideration the time data. Thus we address control synthesis for Timed Discrete Event Systems under MEC specifications by using Timed Petri Nets

by Siu Hing Kee Stanley. / Thesis (M.Phil.)--Chinese University of Hong Kong, 1994. / Includes bibliographical references (leaves 87-88). / Abstract --- p.ii / Acknowledgments --- p.iii / Chapter 1 --- Introduction --- p.1-1 / Chapter 1.1 --- Introduction --- p.1-1 / Chapter 1.2 --- Background --- p.1-2 / Chapter 1.3 --- Thesis Organization --- p.1-4 / Chapter 2 --- Synthesis of Common Structures in a Microcontroller --- p.2-1 / Chapter 2.1 --- Limitation of Synthesis Tools --- p.2-1 / Chapter 2.2 --- Synthesizable VHDL for Common Structures --- p.2-2 / Chapter 2.2.1 --- Counter --- p.2-3 / Chapter 2.2.2 --- Set-Reset Latch --- p.2-6 / Chapter 2.2.3 --- D Latch --- p.2-9 / Chapter 2.2.4 --- D Flip-flop --- p.2-12 / Chapter 2.2.5 --- Multiplexor --- p.2-13 / Chapter 2.2.6 --- Shift Register --- p.2-15 / Chapter 2.2.7 --- Signal Affected by Two Signal Edges --- p.2-18 / Chapter 2.2.8 --- Combinational Feedback --- p.2-19 / Chapter 2.2.9 --- Short Pulses --- p.2-21 / Chapter 2.2.10 --- Register Transfer Logic --- p.2-22 / Chapter 2.2.11 --- Status Flag --- p.2-26 / Chapter 2.2.12 --- Register Access --- p.2-30 / Chapter 2.2.13 --- Clock Divider --- p.2-34 / Chapter 2.2.14 --- Communication among Processes --- p.2-36 / Chapter 3 --- Synthesis of Components of a Microcontroller --- p.3-1 / Chapter 3.1 --- Timer --- p.3-1 / Chapter 3.2 --- Serial Peripheral Interface (SPI) --- p.3-9 / Chapter 3.3 --- Serial Communication Interface (SCI) --- p.3-16 / Chapter 3.4 --- Parallel I/O Port --- p.3-21 / Chapter 3.5 --- 6805CPU --- p.3-22 / Chapter 3.5.1 --- State Counter --- p.3-23 / Chapter 3.5.2 --- Instruction Decoding and Execution Unit --- p.3-24 / Chapter 3.5.3 --- Interrupt Logic --- p.3-25 / Chapter 3.5.4 --- Instruction Register --- p.3-27 / Chapter 4 --- VHDL Coding and Synthesis --- p.4-1 / Chapter 4.1 --- Controlling Synthesis by VHDL Coding --- p.4-1 / Chapter 4.1.1 --- Structure Control --- p.4-2 / Chapter 4.1.2 --- Feedback Path Control --- p.4-2 / Chapter 4.1.3 --- Control of Use of Storage --- p.4-2 / Chapter 4.1.4 --- Timing Control --- p.4-3 / Chapter 4.2 --- Consequences of the Writing Guidelines --- p.4-5 / Chapter 5 --- Interface Tool for Generation of VHDL for a Microcontroller --- p.5-1 / Chapter 5.1 --- Features --- p.5-1 / Chapter 5.2 --- Construction --- p.5-1 / Chapter 5.3 --- Illustration --- p.5-3 / Chapter 5.4 --- Data Structure --- p.5-5 / Chapter 5.4.1 --- Design List --- p.5-6 / Chapter 5.4.2 --- Instance Data --- p.5-6 / Chapter 5.4.3 --- Instance List --- p.5-8 / Chapter 5.4.4 --- Register Data --- p.5-9 / Chapter 5.4.5 --- Dialogs and Functions --- p.5-10 / Chapter 5.5 --- VHDL Generator for Individual Component --- p.5-11 / Chapter 5.6 --- VHDL Generator for the Whole Microcontroller --- p.5-14 / Chapter 6 --- Conclusion --- p.6-1 / Bibliography --- p.B-1 / Appendix --- p.A-1

La vérification à l’exécution est une méthode formelle légère qui consiste à vérifier qu’une exécution d’un système est correcte par rapport à une spécification. La spécification exprime de manière rigoureuse le comportement attendu du système, en utilisant généralement des formalismes basés sur la logique ou les machines à états finies. Alors que la verification a l’éxecution traite les systèmes monolithiques de manière exhaustive, plusieurs difficultés se présentent lors de l’application des techniques existantes à des systèmes décentralisés, c-à-d. des systèmes avec plusieurs composants sans point d’observation central. Dans cette thèse, nous nous concentrons particulièrement sur trois problèmes : la gestion de l’information partielle, la séparation du déploiement des moniteurs du processus de vérification lui-même et le raisonnement sur la décentralisation de manière modulaire et hiérarchique. Nous nous concentrons sur la notion de spécification décentralisée dans laquelle plusieurs spécifications sont fournies pour des parties distinctes du système. Utiliser une spécification décentralisée a divers avantages tels que permettre une synthèse de moniteurs à partir des spécifications complexes et la possibilité de modulariser les spécifications. Nous présentons également un algorithme de vérification général pour les spécifications décentralisées et une structure de données pour représenter l’exécution d’un automate avec observations partielles. Nous développons l’outil THEMIS, qui fournit une plateforme pour concevoir des algorithmes de vérification décentralisée, des mesures pour les algorithmes, une simulation et des expérimentations reproductibles pour mieux comprendre les algorithmes.Nous illustrons notre approche avec diverses applications. Premièrement, nous utilisons des spécifications décentralisées pour munir une analyse de pire cas, adapter, comparer et simuler trois algorithmes de vérification décentralisée existants dans deux scénarios: l’interface graphique Chiron, et des traces et spécifications générées aléatoirement. Deuxièmement, nous utilisons des spécifications décentralisées pour vérifier diverses propriétés dans un appartement intelligent: correction du comportement des capteurs de l’appartement, détection d’activité spécifiques de l’utilisateur (Activities of Daily Living, ADL) et composition de spécifications des deux catégories précédentes.En outre, nous élaborons sur l’utilisation de spécifications décentralisées pour la vérification décentralisée pendant l’exécution de programmes parallélisés. Nous commençons par discuter les limitations des approches et des outils existants lorsque les difficultés introduites par le parallélisme sont rencontrées. Nous détaillons la description de zones de parallélisme d’une unique exécution d’un programme et décrivons une approche générale qui permet de réutiliser des techniques de verification à l’éxécution existantes. Dans notre configuration, les moniteurs sont déployés dans des fils d’exécution spécifiques et échangent de l’information uniquement lorsque des points de synchronisation définis par le programme lui-même sont atteints. En utilisant les points de synchronisation existants, notre approche réduit les interférences et surcoûts résultant de la synchronisation, au prix d’un retard pour déterminer le verdict. / Runtime Verification (RV) is a lightweight formal method which consists in verifying that a run of a system is correct with respect to a specification. The specification formalizes the behavior of the system typically using logics or finite-state machines. While RV comprehensively deals with monolithic systems, multiple challenges are presented when scaling existing approaches to decentralized systems, that is, systems with multiple components with no central observation point. We focus particularly on three challenges: managing partial information, separating monitor deployment from the monitoring process itself, and reasoning about decentralization in a modular and hierarchical way. We present the notion of a decentralized specification wherein multiple specifications are provided for separate parts of the system. Decentralized specifications provide various advantages such as modularity, and allowing for realistic monitor synthesis of the specifications. We also present a general monitoring algorithm for decentralized specifications, and a general datastructure to encode automata execution with partial observations. We develop the THEMIS tool, which provides a platform for designing decentralized monitoring algorithms, metrics for algorithms, and simulation to better understand the algorithms, and design reproducible experiments.We illustrate the approach with two applications. First, we use decentralized specifications to perform a worst-case analysis, adapt, compare, and simulate three existing decentralized monitoring algorithms on both a real example of a user interface, and randomly generated traces and specifications. Second, we use decentralized specifications to check various specifications in a smart apartment: behavioral correctness of the apartment sensors, detection of specific user activities (known as activities of daily living), and composition of properties of the previous types.Furthermore, we elaborate on utilizing decentralized specifications for the decentralized online monitoring of multithreadedprograms. We first expand on the limitations of existing tools and approaches when meeting the challenges introduced by concurrency and ensure that concurrency needs to be taken into account by considering partial orders in traces. We detail the description of such concurrency areas in a single program execution, and provide a general approach which allows re-using existing RV techniques. In our setting, monitors are deployed within specific threads, and only exchange information upon reaching synchronization regions defined by the program itself. By using the existing synchronization, we reduce additional overhead and interference to synchronize at the cost of adding a delay to determine the verdict.

<p>The purpose of this master thesis is to improve the quality of software testing in a large company developing real-time embedded systems. Software testing is a very important part of software development. By performing comprehensive software testing the quality and validity of a software system can be assured. One of the main issues with software testing is to be sure that the tests are correct. Knowing what to test, but also how to perform testing, is of utmost importance.</p><p>In this thesis, we explore different ways to increase the quality of real-time testing by introducing new techniques in several stages of the software development model. Four complementary methods are suggested. The proposed methods are validated by implementing them in an existing and completed project on a subset of the software development process. The original output from the completed project is compared with the new output.</p><p>The presented results from the validation are positive in the sense that it is shown that the test stage was more qualitative, mostly due to a higher level of quality on input from earlier stages.</p>

We discuss a new approach to the construction of software systems. Instead of attempting to build a system that is as free of errors as possible, the designer instead identifies key properties that the execution must satisfy to be acceptable to its users. Together, these properties define the acceptability envelope of the system: the region that it must stay within to remain acceptable. The developer then augments the system with a layered set of components, each of which enforces one of the acceptability properties. The potential advantages of this approach include more flexible, resilient systems that recover from errors and behave acceptably across a wide range of operating environments, an appropriately prioritized investment of engineering resources, and the ability to productively incorporate unreliable components into the final software system. / Singapore-MIT Alliance (SMA)

Η Διπλωματική Εργασία, έχει σαν γενικό σκοπό, την μέσα από βιβλιογραφική έρευνα (κυρίως άρθρων δημοσιευμένων στο Διαδίκτυο), αποσαφήνιση της διαδικασίας δημιουργίας Διεθνών Προτύπων για την Ηλεκτρονική Μάθηση. Για την ικανοποίηση του παραπάνω γενικού σκοπού, επιτεύχθηκαν οι εξής ειδικότεροι: 1. Η καταγραφή της τυπικής διαδικασίας για την δημιουργία de jure και de facto προτύπων για την ηλεκτρονική μάθηση. 2. Η χαρτογράφηση του πλαισίου, σύμφωνα με το οποίο, προκύπτουν οι αναγκαιότητες για την δημιουργία διεθνών προτύπων στην ηλεκτρονική μάθηση. 3. Η καταγραφή των υπαρχόντων διαφοροποιημένων τομέων εργασίας για την δημιουργία διεθνών προτύπων στην ηλεκτρονική μάθηση. 4. Η εύρεση και καταγραφή των κυριοτέρων ινστιτούτων και οργανισμών που συμμετέχουν στην παραπάνω διαδικασία, με αναφορά στην διοικητική δομή, οργάνωση, λειτουργία και στα προϊόντα της εργασίας τους. Επίσης στα πλαίσια του γενικότερου σκοπού, έγινε διερεύνηση και αναφορά και στις πλέον σύγχρονες τάσεις, αυτές της σε συνδυασμό χρησιμοποίησης ήδη υπαρχόντων προτύπων και τεχνικών προδιαγραφών, για την δημιουργία ενός de facto μοντέλου ψηφιακού εκπαιδευτικού συστήματος. / This Postgraduate Work has as general objective, the clarification of the process for the creation of International Standards in Electronic Learning through bibliographic research, mainly of articles published in the Internet. For the satisfaction of this general objective, the following more specialized objectives were achieved: 1. The recording of formal process for the creation de jure and de facto standards in electronic learning. 2. The mapping of frame, according to which, the necessities for the creation of international standards in electronic learning, result. 3. The recording of existing differentiated sectors of work for the creation of international standards in electronic learning. 4. The finding and recording of the most important institutions and organizations which participate in the above process, with reports for their administrative structure, operation and the products of their work. In the frame of the general objective, investigation and report has also been done about the latest modern tendencies. These tendencies refer to the use of combination of already existing standards and technical specifications, for the creation of a de facto model of a digital educational system.