A software tool that generates symbolic model verifier (SMV) input language from a predicate transition net

The purpose of this research was to apply model checking by using a symbolic model checker on Predicate Transition Nets (PrT Nets). A PrT Net is a formal model of information flow which allows system properties to be modeled and analyzed. The aim of this thesis was to use the modeling and analysis power of PrT nets to provide a mechanism for the system model to be verified. Symbolic Model Verifier (SMV) was the model checker chosen in this thesis, and in order to verify the PrT net model of a system, it was translated to SMV input language. A software tool was implemented which translates the PrT Net into SMV language, hence enabling the process of model checking. The system includes two parts: the PrT net editor where the representation of a system can be edited, and the translator which converts the PrT net into an SMV program.

Development and implementation of a tool to assess the micro/macro elements in an organization

This study examines the congruency of planning between organizational structure and process, through an evaluation and planning model known as the Micro/Macro Dynamic Planning Grid. The model compares day-to-day planning within an organization to planning imposed by organizational administration and accrediting agencies. A survey instrument was developed to assess the micro and macro sociological analysis elements utilized by an organization.^ The Micro/Macro Dynamic Planning Grid consists of four quadrants. Each quadrant contains characteristics that reflect the interaction between the micro and macro elements of planning, objectives and goals within an organization. The Over Macro/Over Micro, Quadrant 1, contains attributes that reflect a tremendous amount of action and ongoing adjustments, typical of an organization undergoing significant changes in either leadership, program and/or structure. Over Macro/Under Micro, Quadrant 2, reflects planning characteristics found in large, bureaucratic systems with little regard given to the workings of their component parts. Under Macro/Under Micro, Quadrant 3, reflects the uncooperative, uncoordinated organization, one that contains a multiplicity of viewpoints, language, objectives and goals. Under Macro/Under Micro, Quadrant 4 represents the worst case scenario for any organization. The attributes of this quadrant are very reactive, chaotic, non-productive and redundant.^ There were three phases to the study: development of the initial instrument, pilot testing the initial instrument and item revision, and administration and assessment of the refined instrument. The survey instrument was found to be valid and reliable for the purposes and audiences herein described.^ In order to expand the applicability of the instrument to other organizational settings, the survey was administered to three professional colleges within a university.^ The first three specific research questions collectively answered, in the affirmative, the basic research question: Can the Micro/Macro Dynamic Planning Grid be applied to an organization through an organizational development tool? The first specific question: Can an instrument be constructed that applies the Micro/Macro Dynamic Planning Grid? The second specific research question: Is the constructed instrument valid and reliable? The third specific research question: Does an instrument that applies the Micro/Macro Dynamic Planning Grid assess congruency of micro and macro planning, goals and objectives within an organization? The fourth specific research question: What are the differences in the responses based on roles and responsibilities within an organization? involved statistical analysis of the response data and comparisons obtained with the demographic data. (Abstract shortened by UMI.) ^

A framework for transforming, analyzing, and realizing software designs in unified modeling language

Unified Modeling Language (UML) is the most comprehensive and widely accepted object-oriented modeling language due to its multi-paradigm modeling capabilities and easy to use graphical notations, with strong international organizational support and industrial production quality tool support. However, there is a lack of precise definition of the semantics of individual UML notations as well as the relationships among multiple UML models, which often introduces incomplete and inconsistent problems for software designs in UML, especially for complex systems. Furthermore, there is a lack of methodologies to ensure a correct implementation from a given UML design. The purpose of this investigation is to verify and validate software designs in UML, and to provide dependability assurance for the realization of a UML design.^ In my research, an approach is proposed to transform UML diagrams into a semantic domain, which is a formal component-based framework. The framework I proposed consists of components and interactions through message passing, which are modeled by two-layer algebraic high-level nets and transformation rules respectively. In the transformation approach, class diagrams, state machine diagrams and activity diagrams are transformed into component models, and transformation rules are extracted from interaction diagrams. By applying transformation rules to component models, a (sub)system model of one or more scenarios can be constructed. Various techniques such as model checking, Petri net analysis techniques can be adopted to check if UML designs are complete or consistent. A new component called property parser was developed and merged into the tool SAM Parser, which realize (sub)system models automatically. The property parser generates and weaves runtime monitoring code into system implementations automatically for dependability assurance. The framework in the investigation is creative and flexible since it not only can be explored to verify and validate UML designs, but also provides an approach to build models for various scenarios. As a result of my research, several kinds of previous ignored behavioral inconsistencies can be detected.^

The role of *language in early childhood mathematics

Math literacy is imperative to succeed in society. Experience is key for acquiring math literacy. A preschooler's world is full of mathematical experiences. Children are continually counting, sorting and comparing as they play. As children are engaged in these activities they are using language as a tool to express their mathematical thinking. If teachers are aware of these teachable moments and help children bridge their daily experiences to mathematical concepts, math literacy may be enhanced. This study described the interactions between teachers and preschoolers, determining the extent to which teachers scaffold children's everyday language into expressions of mathematical concepts. Of primary concern were the teachers' responsive interactions to children's expressions of an implicit mathematical utterance made while engaged in block play. The parallel mixed methods research design consisted of two strands. Strand 1 of the study focused on preschoolers' use of everyday language and the teachers' responses after a child made a mathematical utterance. Twelve teachers and 60 students were observed and videotaped while engaged in block play. Each teacher worked with five children for 20 minutes, yielding 240 minutes of observation. Interaction analysis was used to deductively analyze the recorded observations and field notes. Using a priori codes for the five mathematical concepts, it was found children produced 2,831 mathematical utterances. Teachers ignored 60% of these utterances and responded to, but did not mediate 30% of them. Only 10% of the mathematical utterances were mediated to a mathematical concept. Strand 2 focused on the teacher's view of the role of language in early childhood mathematics. The 12 teachers who had been observed as part of the first strand of the study were interviewed. Based on a thematic analysis of these interviews three themes emerged: (a) the importance of a child's environment, (b) the importance of an education in society, and (c) the role of math in early childhood. Finally, based on a meta-inference of both strands, three themes emerged: (a) teacher conception of math, (b) teacher practice, and (c) teacher sensitivity. Implications based on the findings involve policy, curriculum, and professional development.

Foreign Language Education in Colombia: A Qualitative Study of Escuela Nueva

Since 2004 the Colombian Ministry of Education has been implementing the Programa Nacional de Bilingüismo (PNB) with the goal of having bilingual high school graduates in English and Spanish by 2019. However, implementation of the PNB has been criticized by English Language Teaching (ELT) specialists in the country who say, among other things, that the PNB introduced a discourse associated exclusively with bilingualism in English and Spanish. This study analyzed interviews with 15 participants of a public school of the Colombian Escuela Nueva, a successful model of community-based education that has begun a process of internationalization, regarding the participants’ perceptions of foreign language education and the policies of the PNB. Six students, five teachers, and four administrators were each interviewed twice using semi-structured interviews. To offer a critique of the PNB, this study tried to determine to what extent the school implemented the elements of Responsible ELT, a model developed by the researcher incorporating the concepts of hegemony of English, critical language-policy research, and resistance in ELT. Findings included the following: (a) students and teachers saw English as the universal language whereas most administrators saw English imposed due to political and economic reasons; (b) some teachers misinterpreted the 1994 General Law of Education mandating the teaching of a foreign language as a law mandating English; and (c) some teachers and administrators saw the PNB’s adoption of competence standards based on the Common European Framework of Reference for languages as beneficial whereas others saw it as arbitrary. Conclusions derived from this study of this Escuela Nueva school were: (a) most participants found the goal of the PNB unrealistic; (b) most teachers and administrators saw the policies of the PNB as top-down policies without assessment or continuity; and (c) teachers and administrators mentioned a disarticulation between elementary and high school ELT policies that may be discouraging students in public schools from learning English. Thus, this study suggests that the policies of the PNB may be contributing to English becoming a gatekeeper for higher education and employment thereby becoming a tool for sustaining inequality in Colombia.