A Model-Based Development and Verification Framework for Distributed System-on-Chip Architecture

The capabilities and thus, design complexity of VLSI-based embedded systems have increased tremendously in recent years, riding the wave of Moore’s law. The time-to-market requirements are also shrinking, imposing challenges to the designers, which in turn, seek to adopt new design methods to increase their productivity. As an answer to these new pressures, modern day systems have moved towards on-chip multiprocessing technologies. New architectures have emerged in on-chip multiprocessing in order to utilize the tremendous advances of fabrication technology. Platform-based design is a possible solution in addressing these challenges. The principle behind the approach is to separate the functionality of an application from the organization and communication architecture of hardware platform at several levels of abstraction. The existing design methodologies pertaining to platform-based design approach don’t provide full automation at every level of the design processes, and sometimes, the co-design of platform-based systems lead to sub-optimal systems. In addition, the design productivity gap in multiprocessor systems remain a key challenge due to existing design methodologies. This thesis addresses the aforementioned challenges and discusses the creation of a development framework for a platform-based system design, in the context of the SegBus platform - a distributed communication architecture. This research aims to provide automated procedures for platform design and application mapping. Structural verification support is also featured thus ensuring correct-by-design platforms. The solution is based on a model-based process. Both the platform and the application are modeled using the Unified Modeling Language. This thesis develops a Domain Specific Language to support platform modeling based on a corresponding UML profile. Object Constraint Language constraints are used to support structurally correct platform construction. An emulator is thus introduced to allow as much as possible accurate performance estimation of the solution, at high abstraction levels. VHDL code is automatically generated, in the form of “snippets” to be employed in the arbiter modules of the platform, as required by the application. The resulting framework is applied in building an actual design solution for an MP3 stereo audio decoder application.

Problem solving and computer-assisted instruction in science education : analysis of research findings and the research process /

The quantitative component of this study examined the effect of computerassisted instruction (CAI) on science problem-solving performance, as well as the significance of logical reasoning ability to this relationship. I had the dual role of researcher and teacher, as I conducted the study with 84 grade seven students to whom I simultaneously taught science on a rotary-basis. A two-treatment research design using this sample of convenience allowed for a comparison between the problem-solving performance of a CAI treatment group (n = 46) versus a laboratory-based control group (n = 38). Science problem-solving performance was measured by a pretest and posttest that I developed for this study. The validity of these tests was addressed through critical discussions with faculty members, colleagues, as well as through feedback gained in a pilot study. High reliability was revealed between the pretest and the posttest; in this way, students who tended to score high on the pretest also tended to score high on the posttest. Interrater reliability was found to be high for 30 randomly-selected test responses which were scored independently by two raters (i.e., myself and my faculty advisor). Results indicated that the form of computer-assisted instruction (CAI) used in this study did not significantly improve students' problem-solving performance. Logical reasoning ability was measured by an abbreviated version of the Group Assessment of Lx)gical Thinking (GALT). Logical reasoning ability was found to be correlated to problem-solving performance in that, students with high logical reasoning ability tended to do better on the problem-solving tests and vice versa. However, no significant difference was observed in problem-solving improvement, in the laboratory-based instruction group versus the CAI group, for students varying in level of logical reasoning ability.Insignificant trends were noted in results obtained from students of high logical reasoning ability, but require further study. It was acknowledged that conclusions drawn from the quantitative component of this study were limited, as further modifications of the tests were recommended, as well as the use of a larger sample size. The purpose of the qualitative component of the study was to provide a detailed description ofmy thesis research process as a Brock University Master of Education student. My research journal notes served as the data base for open coding analysis. This analysis revealed six main themes which best described my research experience: research interests, practical considerations, research design, research analysis, development of the problem-solving tests, and scoring scheme development. These important areas ofmy thesis research experience were recounted in the form of a personal narrative. It was noted that the research process was a form of problem solving in itself, as I made use of several problem-solving strategies to achieve desired thesis outcomes.

A qualitative journey into cyberspace /

Educators should movefrom teacher-centered learning to student-centered learning, from isolated work to collaborative work, andfromfactual knowledgebased instructions to critical thinking and informed decision-making. The high tech classroom should be more interactive and encourage active, exploratory, inquiry-based learning, as opposed to the didactic mode in which teachersfeed students information. (Valenti,2000, p. 85) The influence of technology in schools is growing as quickly as the students it impacts. As a pioneer in an e-leaming high school, I hoped to better understand the effects and influences of this learning tool in the English classroom. Using interpretive ethnography as my main frame of reference, I examined the role of technology in a grade 9 Academic English class environment. My role was participant observer as I worked with 4 students in the Laptop Program at St. Augustine Catholic High School. Through interview, observation, joumaling, and thick description, I undertook a journey into cyberspace. I documented the experiences, the frustrations, and the highlights of being in e-leaming along with my students. In this study, I specifically considered the issues of teacher training, administrative support, technology support personnel, resource availability, the role of the teacher in a constructivist classroom, and the benefits of the laptop computer as a learning tool in classroom and school.

Winâ Foy : functional object-oriented programming language

This thesis will introduce a new strongly typed programming language utilizing Self types, named Win--*Foy, along with a suitable user interface designed specifically to highlight language features. The need for such a programming language is based on deficiencies found in programming languages that support both Self types and subtyping. Subtyping is a concept that is taken for granted by most software engineers programming in object-oriented languages. Subtyping supports subsumption but it does not support the inheritance of binary methods. Binary methods contain an argument of type Self, the same type as the object itself, in a contravariant position, i.e. as a parameter. There are several arguments in favour of introducing Self types into a programming language (11. This rationale led to the development of a relation that has become known as matching [4, 5). The matching relation does not support subsumption, however, it does support the inheritance of binary methods. Two forms of matching have been proposed (lJ. Specifically, these relations are known as higher-order matching and I-bound matching. Previous research on these relations indicates that the higher-order matching relation is both reflexive and transitive whereas the f-bound matching is reflexive but not transitive (7]. The higher-order matching relation provides significant flexibility regarding inheritance of methods that utilize or return values of the same type. This flexibility, in certain situations, can restrict the programmer from defining specific classes and methods which are based on constant values [21J. For this reason, the type This is used as a second reference to the type of the object that cannot, contrary to Self, be specialized in subclasses. F-bound matching allows a programmer to define a function that will work for all types of A', a subtype of an upper bound function of type A, with the result type being dependent on A'. The use of parametric polymorphism in f-bound matching provides a connection to subtyping in object-oriented languages. This thesis will contain two main sections. Firstly, significant details concerning deficiencies of the subtype relation and the need to introduce higher-order and f-bound matching relations into programming languages will be explored. Secondly, a new programming language named Win--*Foy Functional Object-Oriented Programming Language has been created, along with a suitable user interface, in order to facilitate experimentation by programmers regarding the matching relation. The construction of the programming language and the user interface will be explained in detail.

Region Connection Calculus: Composition Tables and Constraint Satisfaction Problems

Qualitative spatial reasoning (QSR) is an important field of AI that deals with qualitative aspects of spatial entities. Regions and their relationships are described in qualitative terms instead of numerical values. This approach models human based reasoning about such entities closer than other approaches. Any relationships between regions that we encounter in our daily life situations are normally formulated in natural language. For example, one can outline one's room plan to an expert by indicating which rooms should be connected to each other. Mereotopology as an area of QSR combines mereology, topology and algebraic methods. As mereotopology plays an important role in region based theories of space, our focus is on one of the most widely referenced formalisms for QSR, the region connection calculus (RCC). RCC is a first order theory based on a primitive connectedness relation, which is a binary symmetric relation satisfying some additional properties. By using this relation we can define a set of basic binary relations which have the property of being jointly exhaustive and pairwise disjoint (JEPD), which means that between any two spatial entities exactly one of the basic relations hold. Basic reasoning can now be done by using the composition operation on relations whose results are stored in a composition table. Relation algebras (RAs) have become a main entity for spatial reasoning in the area of QSR. These algebras are based on equational reasoning which can be used to derive further relations between regions in a certain situation. Any of those algebras describe the relation between regions up to a certain degree of detail. In this thesis we will use the method of splitting atoms in a RA in order to reproduce known algebras such as RCC15 and RCC25 systematically and to generate new algebras, and hence a more detailed description of regions, beyond RCC25.

Perceptions of Technology and Manifestations of Language Learner Autonomy

a grounded theory study investigating perceptions of technology by learners of English as a second language

L-Fuzzy Structured Query Language

Lattice valued fuzziness is more general than crispness or fuzziness based on the unit interval. In this work, we present a query language for a lattice based fuzzy database. We define a Lattice Fuzzy Structured Query Language (LFSQL) taking its membership values from an arbitrary lattice L. LFSQL can handle, manage and represent crisp values, linear ordered membership degrees and also allows membership degrees from lattices with non-comparable values. This gives richer membership degrees, and hence makes LFSQL more flexible than FSQL or SQL. In order to handle vagueness or imprecise information, every entry into an L-fuzzy database is an L-fuzzy set instead of crisp values. All of this makes LFSQL an ideal query language to handle imprecise data where some factors are non-comparable. After defining the syntax of the language formally, we provide its semantics using L-fuzzy sets and relations. The semantics can be used in future work to investigate concepts such as functional dependencies. Last but not least, we present a parser for LFSQL implemented in Haskell.

Approche cognitive de la traduction dans les langues de spécialité : vers une systématisation de la description de la conceptualisation métaphorique

Département de linguistique et de traduction

A Type-Preserving Compiler from System F to Typed Assembly Language

L'utilisation des méthodes formelles est de plus en plus courante dans le développement logiciel, et les systèmes de types sont la méthode formelle qui a le plus de succès. L'avancement des méthodes formelles présente de nouveaux défis, ainsi que de nouvelles opportunités. L'un des défis est d'assurer qu'un compilateur préserve la sémantique des programmes, de sorte que les propriétés que l'on garantit à propos de son code source s'appliquent également au code exécutable. Cette thèse présente un compilateur qui traduit un langage fonctionnel d'ordre supérieur avec polymorphisme vers un langage assembleur typé, dont la propriété principale est que la préservation des types est vérifiée de manière automatisée, à l'aide d'annotations de types sur le code du compilateur. Notre compilateur implante les transformations de code essentielles pour un langage fonctionnel d'ordre supérieur, nommément une conversion CPS, une conversion des fermetures et une génération de code. Nous présentons les détails des représentation fortement typées des langages intermédiaires, et les contraintes qu'elles imposent sur l'implantation des transformations de code. Notre objectif est de garantir la préservation des types avec un minimum d'annotations, et sans compromettre les qualités générales de modularité et de lisibilité du code du compilateur. Cet objectif est atteint en grande partie dans le traitement des fonctionnalités de base du langage (les «types simples»), contrairement au traitement du polymorphisme qui demande encore un travail substantiel pour satisfaire la vérification de type.

Sur l’utilisation du langage de programmation Scheme pour le développement de jeux vidéo

Ce mémoire vise à recenser les avantages et les inconvénients de l'utilisation du langage de programmation fonctionnel dynamique Scheme pour le développement de jeux vidéo. Pour ce faire, la méthode utilisée est d'abord basée sur une approche plus théorique. En effet, une étude des besoins au niveau de la programmation exprimés par ce type de développement, ainsi qu'une description détaillant les fonctionnalités du langage Scheme pertinentes au développement de jeux vidéo sont données afin de bien mettre en contexte le sujet. Par la suite, une approche pratique est utilisée en effectuant le développement de deux jeux vidéo de complexités croissantes: Space Invaders et Lode Runner. Le développement de ces jeux vidéo a mené à l'extension du langage Scheme par plusieurs langages spécifiques au domaine et bibliothèques, dont notamment un système de programmation orienté objets et un système de coroutines. L'expérience acquise par le développement de ces jeux est finalement comparée à celle d'autres développeurs de jeux vidéo de l'industrie qui ont utilisé Scheme pour la création de titres commerciaux. En résumé, l'utilisation de ce langage a permis d'atteindre un haut niveau d'abstraction favorisant la modularité des jeux développés sans affecter les performances de ces derniers.

A lexical semantic study of Dene Suliné, an Athabaskan language

Cette thèse constitue une étude systématique du lexique du déné sųłiné, une langue athabaskane du nord-ouest canadien. Elle présente les définitions et les patrons de combinatoire syntaxique et lexicale de plus de 200 unités lexicales, lexèmes et phrasèmes, qui représentent une partie importante du vocabulaire déné sųłiné dans sept domaines: les émotions, le caractère humain, la description physique des entités, le mouvement des êtres vivants, la position des entités, les conditions atmospheriques et les formations topologiques, en les comparant avec le vocubulaire équivalent de l'anglais. L’approche théorique choisie est la Théorie Sens-Texte (TST), une approche formelle qui met l’accent sur la description sémantique et lexicographique empiriques. La présente recherche relève d'importantes différences entre le lexique du déné sųłiné et celui de l'anglais à tous les niveaux: dans la correspondence entre la représentation conceptuelle, considérée (quasi-)extralinguistique, et la structure sémantique; dans les patrons de lexicalisation des unités lexicales, et dans les patrons de combinatoire syntaxique et lexicale, qui montrent parfois des traits propres au déné sųłiné intéressants.

L’erreur lexicale au secondaire : analyse d’erreurs lexicales d’élèves de 3e secondaire et description du rapport à l’erreur lexicale d’enseignants de français

Cette recherche vise à décrire 1) les erreurs lexicales commises en production écrite par des élèves francophones de 3e secondaire et 2) le rapport à l’erreur lexicale d’enseignants de français (conception de l’erreur lexicale, pratiques d’évaluation du vocabulaire en production écrite, modes de rétroaction aux erreurs lexicales). Le premier volet de la recherche consiste en une analyse d’erreurs à trois niveaux : 1) une description linguistique des erreurs à l’aide d’une typologie, 2) une évaluation de la gravité des erreurs et 3) une explication de leurs sources possibles. Le corpus analysé est constitué de 300 textes rédigés en classe de français par des élèves de 3e secondaire. L’analyse a révélé 1144 erreurs lexicales. Les plus fréquentes sont les problèmes sémantiques (30%), les erreurs liées aux propriétés morphosyntaxiques des unités lexicales (21%) et l’utilisation de termes familiers (17%). Cette répartition démontre que la moitié des erreurs lexicales sont attribuables à une méconnaissance de propriétés des mots autres que le sens et la forme. L’évaluation de la gravité des erreurs repose sur trois critères : leur acceptation linguistique selon les dictionnaires, leur impact sur la compréhension et leur degré d’intégration à l’usage. Les problèmes liés aux registres de langue sont généralement ceux qui sont considérés comme les moins graves et les erreurs sémantiques représentent la quasi-totalité des erreurs graves. Le troisième axe d’analyse concerne la source des erreurs et fait ressortir trois sources principales : l’influence de la langue orale, la proximité sémantique et la parenté formelle entre le mot utilisé et celui visé. Le second volet de la thèse concerne le rapport des enseignants de français à l’erreur lexicale et repose sur l’analyse de 224 rédactions corrigées ainsi que sur une série de huit entrevues menées avec des enseignants de 3e secondaire. Lors de la correction, les enseignants relèvent surtout les erreurs orthographiques ainsi que celles relevant des propriétés morphosyntaxiques des mots (genre, invariabilité, régime), qu’ils classent parmi les erreurs de grammaire. Les erreurs plus purement lexicales, c’est-à-dire les erreurs sémantiques, l’emploi de termes familiers et les erreurs de collocation, demeurent peu relevées, et les annotations des enseignants concernant ces types d’erreurs sont vagues et peu systématiques, donnant peu de pistes aux élèves pour la correction. L’évaluation du vocabulaire en production écrite est toujours soumise à une appréciation qualitative, qui repose sur l’impression générale des enseignants plutôt que sur des critères précis, le seul indicateur clair étant la répétition. Les explications des enseignants concernant les erreurs lexicales reposent beaucoup sur l’intuition, ce qui témoigne de certaines lacunes dans leur formation en lien avec le vocabulaire. Les enseignants admettent enseigner très peu le vocabulaire en classe au secondaire et expliquent ce choix par le manque de temps et d’outils adéquats. L’enseignement du vocabulaire est toujours subordonné à des tâches d’écriture ou de lecture et vise davantage l’acquisition de mots précis que le développement d’une réelle compétence lexicale.

A Compiler for the dependently typed language Beluga

Les structures avec des lieurs sont très communes en informatique. Les langages de programmation et les systèmes logiques sont des exemples de structures avec des lieurs. La manipulation de lieurs est délicate, de sorte que l’écriture de programmes qui ma- nipulent ces structures tirerait profit d’un soutien spécifique pour les lieurs. L’environ- nement de programmation Beluga est un exemple d’un tel système. Nous développons et présentons ici un compilateur pour ce système. Parmi les programmes pour lesquels Beluga est spécialement bien adapté, plusieurs peuvent bénéficier d’un compilateur. Par exemple, les programmes pour valider les types (les "type-checkers"), les compilateurs et les interpréteurs tirent profit du soutien spécifique des lieurs et des types dépendants présents dans le langage. Ils nécessitent tous également une exécution efficace, que l’on propose d’obtenir par le biais d’un compilateur. Le but de ce travail est de présenter un nouveau compilateur pour Beluga, qui emploie une représentation interne polyvalente et permet de partager du code entre plusieurs back-ends. Une contribution notable est la compilation du filtrage de Beluga, qui est particulièrement puissante dans ce langage.

Intégration de services de raisonnement automatique basés sur les logiques de description dans les applications d’entreprise

Ce mémoire présente un patron d’architecture permettant, dans un contexte orientéobjet, l’exploitation d’objets appartenant simultanément à plusieurs hiérarchies fonctionnelles. Ce patron utilise un reasoner basé sur les logiques de description (web sémantique) pour procéder à la classification des objets dans les hiérarchies. La création des objets est simplifiée par l’utilisation d’un ORM (Object Relational Mapper). Ce patron permet l’utilisation effective du raisonnement automatique dans un contexte d’applications d’entreprise. Les concepts requis pour la compréhension du patron et des outils sont présentés. Les conditions d’utilisation du patron sont discutées ainsi que certaines pistes de recherche pour les élargir. Un prototype appliquant le patron dans un cas simple est présenté. Une méthodologie accompagne le patron. Finalement, d’autres utilisations potentielles des logiques de description dans le même contexte sont discutées.

Parallelization of SAT on Reconfigurable Hardware

Quoique très difficile à résoudre, le problème de satisfiabilité Booléenne (SAT) est fréquemment utilisé lors de la modélisation d’applications industrielles. À cet effet, les deux dernières décennies ont vu une progression fulgurante des outils conçus pour trouver des solutions à ce problème NP-complet. Deux grandes avenues générales ont été explorées afin de produire ces outils, notamment l’approche logicielle et matérielle. Afin de raffiner et améliorer ces solveurs, de nombreuses techniques et heuristiques ont été proposées par la communauté de recherche. Le but final de ces outils a été de résoudre des problèmes de taille industrielle, ce qui a été plus ou moins accompli par les solveurs de nature logicielle. Initialement, le but de l’utilisation du matériel reconfigurable a été de produire des solveurs pouvant trouver des solutions plus rapidement que leurs homologues logiciels. Cependant, le niveau de sophistication de ces derniers a augmenté de telle manière qu’ils restent le meilleur choix pour résoudre SAT. Toutefois, les solveurs modernes logiciels n’arrivent toujours pas a trouver des solutions de manière efficace à certaines instances SAT. Le but principal de ce mémoire est d’explorer la résolution du problème SAT dans le contexte du matériel reconfigurable en vue de caractériser les ingrédients nécessaires d’un solveur SAT efficace qui puise sa puissance de calcul dans le parallélisme conféré par une plateforme FPGA. Le prototype parallèle implémenté dans ce travail est capable de se mesurer, en termes de vitesse d’exécution à d’autres solveurs (matériels et logiciels), et ce sans utiliser aucune heuristique. Nous montrons donc que notre approche matérielle présente une option prometteuse vers la résolution d’instances industrielles larges qui sont difficilement abordées par une approche logicielle.