Orientador : Neusa Maria Mendes de Gusmão / Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Educação / Made available in DSpace on 2018-08-03T22:24:00Z (GMT). No. of bitstreams: 1 Abib_PedroRodolphoJungers_D.pdf: 7405091 bytes, checksum: 0acce58b13a2a347753798f1b3aa42dd (MD5) Previous issue date: 2004 / Doutorado

Orientador: Olga Rodrigues de Moraes Von Simson / Dissertação (mestrado) - Universidade Estadual de Campinas, Faculdade de Educação / Made available in DSpace on 2018-07-24T09:10:04Z (GMT). No. of bitstreams: 1 Fernandes_RenataSieiro_M.pdf: 47338946 bytes, checksum: 0f74d226472d1c36917f0031e0f66702 (MD5) Previous issue date: 1998 / Resumo: Esta pesquisa buscou estudar e compreender as relações entre inrancia, cultura e circularidade cultural, imaginário e imaginação, e lúdico através de atividades de jogos e brincadeiras e das interações entre crianças, jovens e adultos que se encontram diariamente em um espaço de educação não-escolar. Espaço este que, apesar da proposta de oferecer atividades e oportunidades de vivências de teor não-escolarizante, ainda assim, acaba marcado por viéses escolares e por contradições entre objetivos pensados e práticas efetivas.Além disso, as próprias relações entre crianças, jovens e adultos, permeadas por repertórios culturais específicos que norte iam formas de ver, sentir e lidar desses grupos, envolvem situações de conflito mas também de encontros de desejos, necessidades e posturas que, por sua vez, implicam nos modos como entendem, encaminham e participam de atividades de brincar, mais especificamente. Para tanto, buscou-se trabalhar com materiais e documentos de diferentes origens, principalmente os construídos com a participação dos envolvidos na pesquisa: observação participante, narrativas de inrancia, entrevistas informais e registros imagéticos: desenhos e fotografias, visando relacionar a bibliografia com o trabalho de pesquisa em campo e Vice-versa / Abstract: This research aimed to study and undestand the relations between childhood, cuIture and circulating culture, imaginary and imagination, and the Iudic ativities, through pIays and games and the relationship between children, teenagers and adults who interact daily in a non-formal educational institution. AIthough this pIace intends to offer activities and living opportunities of non-schooling characteristics, it shows schooling aspects enphasized by the contraditions between aimed proposes and the real practices. In addition, the relationship between chiIdren, teenagers, adults, based on specific cultural repertories which shows how these groups see and feel the world. It, generally, cretes not only conflict situations but also interactions between the aspirations, needs and behavior, which generate ways of understanding, and participating in pIaying activities, more specificaly. In order to do that, it was aimed to work with materiaIs and documents of different origins; particularly those that were produced with the participation of the subjects involved in this research: participative observation, childhood narratives, informal interviews and image registers: drawings and photografies, trying to relate the bibliography with the field research and vice-versa / Mestrado / Ciencias Sociais Aplicadas à Educação / Mestre em Educação

D.Phil. (Computer Science) / Please refer to full text to view abstract

Protocol verification is an exciting area of network security that intersects engineering and formal methods. This thesis presents a comparison of formal verification tools for security protocols for their respective strengths and weaknesses supported by the results from several case studies. The formal verification tools considered are based on explicit model checking (SPIN), symbolic analysis (Proverif) and theorem proving (Coq). We formalize and provide models of several well-known authentication and key-establishment protocols in each of the specification languages, and use the tools to find attacks that show protocols insecurity. We contrast the modelling process on each of the tools by comparing features of their modelling languages, verification efforts involved, and analysis results Our results show that authentication and key-establishment protocols can be specified in Coq’s modeling language with an unbounded number of sessions and message space. However, proofs in Coq require human guidance. SPIN runs automated verification with a restricted version of the Dolev-Yao attacker model. Proverif has several advantages over SPIN and Coq: a tailored specification language, and better performance on infinite state space analysis.

M.Ed. / This study focuses on research conducted at a non-formal adult basic education centre in South Hills, Johannesburg. The research population consists of five women who are migrant, domestic helpers. Levels of literacy within the group range from English Literacy Level Three to non-literacy. In their vernacular languages the participants show varying degrees of literacy or the absence thereof. The research seeks to establish how a specific group of adults learn. This is done by documenting the learning experiences of the group of learners over a period of time. Crucial to the process was providing answers to the following research questions: 1) How do adults learn in non-formal education? and 2) How do collaboration and mediation impact on adult learning in non-formal education? The above research is contextualised within theories of learning which prioritise collaboration and mediation as central to the process. Data collection took place with the research questions foregrounded within the theoretical perspectives indicated above. Sets of binary themes emerged from the research data which are inextricably linked to collaboration and mediation. It is consequently concluded that collaboration and mediation are crucial to processes of learning among the group of adult learners researched and it may therefore be inferred, inductively, that collaboration and mediation could work successfully in similar educational settings. It is consequently recommended that adult education centres incorporate and replicate, in their didactical approaches, the successful methodology utilised in this study.

Ph.D. (Computer Science) / Traditionally a formal language can be characterized in two ways: by a generative device (a grammar) and an acceptive device (an automaton). The characterization of two- and three-dimensional Random Context Grammars by two- and three-dimensional Random Context Automata are investigated. This thesis is an attempt to progressively extend a certain class of grammars to higher dimensions where the class of languages generated in each dimension is contained in the class of languages generated in the next higher dimension. Random Context Array Automata which characterizes Random Context Array Grammars (Von Solms [4,5]) are defined. The power of both Random Context Array Grammars and Random Context Array Automata is inherent in the fact that the replacement of symbols in figures is subject to horizontal, vertical and global context. A proof is given for the equivalence of the class of languages generated by Random Context Array Grammars and the class of languages accepted by Random Context Array Automata. The two-dimensional Random Context Array Grammars are extended to three dimensions. Random Context Structure Grammars generate three-dimensional structures. A characteristic of Random Context Structure Grammars is that the replacement of symbols in a structure is subject to seven relevant contexts. Random Context Structure Automata which characterize Random Context Structure Grammars are defined. It is shown that the class of languages generated by Random Context Structure Grammars are equivalent to the class of languages accepted by Random Context Array Automata...

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. There are two issues in using HLPNs - modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.

This case study analysis looks at four communities in Rift Valley, Kenya including Matisi, Moi’s Bridge, Sirende and Waitaluk. The research focuses on the role of markets in achieving food and livelihood security for the smallholders in these communities and smallholders’ perceptions of the roles of the Government of Kenya and other institutions in facilitating market access. The largest challenges to market participation, as reported by the smallholders in the studied communities, include low yields, weather inconsistencies, and lack of land. In terms of the Government of Kenya, many smallholders noted the benefits of participating in groups as they are subsequently offered training or field days and subsidies. A significant group of respondents did comment on their lack of interest in joining similar groups as they were seen as unstable or corrupt. The potential roles of formal and informal markets to increase food security were also analyzed. All smallholders wished to be participating in informal markets, but twenty-five percent were constrained by the lack of surplus produce. Similarly, although many reported their desire to be participants in formal markets lack of surplus produce, price fluctuations, inconsistent weather patterns, transportation costs and post- harvest losses or food waster were recognized as significant barriers. In order to mitigate these constraints, most smallholders recommended subsidies on inputs and the overall restructuring of markets. It is recommended that organizations and governments implement a livelihood diversification policy program or initiative to diversify and intensify agricultural activities and other non-agricultural activities. This case study analysis demonstrates the need to recognize the importance of local contexts, specifically Rift Valley as much of the research done in Kenya is found in Nairobi and surrounding areas and cautions labeling communities as food secure based on favorable conditions.

We present the design and implementation of a Certified Core Policy Language (ACCPL) that can be used to express access-control rules and policies. Although full-blown access-control policy languages such as eXtensible Access Control Markup Language (XACML) [OAS13] already exist, because access rules in such languages are often expressed in a declarative manner using fragments of a natural language like English, it isn’t alwaysclear what the intended behaviour of the system encoded in these access rules should be. To remedy this ambiguity, formal specification of how an access-control mechanism should behave, is typically given in some sort of logic, often a subset of first order logic. To show that an access-control system actually behaves correctly with respect to its specification, proofs are needed, however the proofs that are often presented in the literature are hard or impossible to formally verify. The verification difficulty is partly due to the fact that the language used to do the proofs while mathematical in nature, utilizes intuitive justifications to derive the proofs. Intuitive language in proofs means that the proofs could be incomplete and/or contain subtle errors. ACCPL is small by design. By small we refer to the size of the language; the syntax, auxiliary definitions and the semantics of ACCPL only take a few pages to describe. This compactness allows us to concentrate on the main goal of this thesis which is the ability to reason about the policies written in ACCPL with respect to specific questions. By making the language compact, we have stayed away from completeness and expressive power in several directions. For example, ACCPL uses only a single policy combinator, the conjunction policy combinator. The design of ACCPL is therefore a trade-off between ease of formal proof of correctness and expressive power. We also consider ACCPL a core policy access-control language since we have retained the core features of many access-control policy languages. For instance ACCPL employs a single condition type called a “prerequisite” where other languages may have very expressive and rich sets of conditions.

A hybrid dynamical system is a mathematical model for a part of the real world where discrete and continuous parts interact with each other. Typically such systems are complex, and it is difficult to know how they will behave for general parameters and initial conditions. However, the method of formal verification gives us the ability to prove automatically that certain behaviour does or does not happen for a range of parameters in a system. The challenge is then to define suitable methods for proving properties on hybrid systems.This thesis looks at using formal verification for proving liveness properties on hybrid systems: a liveness property says that something good eventually happens in the system. This work presents the theoretical background and practical application of various methods for proving and disproving inevitability properties (a type of liveness) in different classes of hybrid systems. The methods combine knowledge of dynamical behaviour of a system with the brute-force approach of model checking, in order to make the most of the benefits of both sides. The work on proving liveness properties is based on abstraction of dynamical systems to timed automata. This thesis explores the limits of a pre-defined abstraction method, adds some dynamical knowledge to the method, and shows that this improvement makes liveness properties provable in certain continuous dynamical systems. The limits are then pushed further to see how this method can be used for piecewise-continuous dynamical systems. The resulting algorithms are implemented for both classes of systems.In order to disprove liveness properties in hybrid systems a novel framework is proposed, using a new property called deadness. Deadness is a dynamically-aware property of the hybrid system which, if true, disproves the liveness property by means of a finite execution: we usually require an infinite execution to disprove a liveness property. An algorithm is proposed which uses dynamical properties of hybrid systems to derive deadness properties automatically, and the implementation of this algorithm is discussed and applied to a simplified model of an oilwell drillstring.