JCircus 2.0: Uma extensão da ferramenta de tradução de Circus para Java

This dissertation aims at extending the JCircus tool, a translator of formal specifications into code that receives a Circus specification as input, and translates the specification into Java code. Circus is a formal language whose syntax is based on Z s and CSP s syntax. JCircus generated code uses JCSP, which is a Java API that implements CSP primitives. As JCSP does not implement all CSP s primitives, the translation strategy from Circus to Java is not trivial. Some CSP primitives, like parallelism, external choice, communication and multi-synchronization are partially implemented. As an aditional scope, this dissertation will also develop a tool for testing JCSP programs, called JCSPUnit, which will also be included in JCircus new version. The extended version of JCircus will be called JCircus 2.0.

Contribuições para verificação automática de applets javacard

The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification

BTS:uma ferramenta de suporte ao desenvolvimento sistemático de sistemas confiáveis baseados em componentes

The component-based development of systems revolutionized the software development process, facilitating the maintenance, providing more confiability and reuse. Nevertheless, even with all the advantages of the development of components, their composition is an important concern. The verification through informal tests is not enough to achieve a safe composition, because they are not based on formal semantic models with which we are able to describe precisally a system s behaviour. In this context, formal methods provide ways to accurately specify systems through mathematical notations providing, among other benefits, more safety. The formal method CSP enables the specification of concurrent systems and verification of properties intrinsic to them, as well as the refinement among different models. Some approaches apply constraints using CSP, to check the behavior of composition between components, assisting in the verification of those components in advance. Hence, aiming to assist this process, considering that the software market increasingly requires more automation, reducing work and providing agility in business, this work presents a tool that automatizes the verification of composition among components, in which all complexity of formal language is kept hidden from users. Thus, through a simple interface, the tool BST (BRIC-Tool-Suport) helps to create and compose components, predicting, in advance, undesirable behaviors in the system, such as deadlocks

Estudo sobre as expressões idiomáticas e o uso de dicionários especiais da língua portuguesa no ensino fundamental

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Pequenas criaturas e o efeito de real: a estética da crueldade em Rubem Fonseca

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Estudando geometria através de dobraduras

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Perigo, probabilidade e oportunidade: a linguagem dos riscos na mídia

Partindo do pressuposto que risco é um conceito central na sociedade contemporânea, este estudo teve por objetivo entender o papel da mídia na circulação e consolidação da linguagem dos riscos. Tendo por base estudos anteriores, optou-se por trabalhar com um único jornal, a Folha de S. Paulo, sendo adotados três procedimentos de pesquisa: 1) mapeamento da diversidade de termos utilizados para falar sobre a possibilidade de ocorrência de eventos concebidos como ocasião para ganho ou perda; 2) análise diacrônica de uma amostra representativa de matérias com a palavra risco no título (1921 e 1998); 3) análise do uso da linguagem de risco por área temática (CD-Rom Folha, 1994-1997). Os resultados sugerem que o uso da linguagem dos riscos na mídia é recente e diversificado, apoiando-se ora na linguagem formal do cálculo de risco, ora no uso metafórico do termo, para falar de desordem na sociedade contemporânea.

Formalizing languages for service oriented computing

Service Oriented Computing is a new programming paradigm for addressing distributed system design issues. Services are autonomous computational entities which can be dynamically discovered and composed in order to form more complex systems able to achieve different kinds of task. E-government, e-business and e-science are some examples of the IT areas where Service Oriented Computing will be exploited in the next years. At present, the most credited Service Oriented Computing technology is that of Web Services, whose specifications are enriched day by day by industrial consortia without following a precise and rigorous approach. This PhD thesis aims, on the one hand, at modelling Service Oriented Computing in a formal way in order to precisely define the main concepts it is based upon and, on the other hand, at defining a new approach, called bipolar approach, for addressing system design issues by synergically exploiting choreography and orchestration languages related by means of a mathematical relation called conformance. Choreography allows us to describe systems of services from a global view point whereas orchestration supplies a means for addressing such an issue from a local perspective. In this work we present SOCK, a process algebra based language inspired by the Web Service orchestration language WS-BPEL which catches the essentials of Service Oriented Computing. From the definition of SOCK we will able to define a general model for dealing with Service Oriented Computing where services and systems of services are related to the design of finite state automata and process algebra concurrent systems, respectively. Furthermore, we introduce a formal language for dealing with choreography. Such a language is equipped with a formal semantics and it forms, together with a subset of the SOCK calculus, the bipolar framework. Finally, we present JOLIE which is a Java implentation of a subset of the SOCK calculus and it is part of the bipolar framework we intend to promote.

Architettura delle centrali idroelettriche italiane 1910-1940. L'esperienza di Giovanni Muzio e Piero Portaluppi

Oggetto della ricerca è il tema dello spazio delle centrali idroelettriche costruite nella prima metà del Novecento dagli architetti Giovanni Muzio e Piero Portaluppi. L’individuazione del tema sorge dalla volontà di indagare quali siano stati gli sviluppi dal punto di vista architettonico all’interno di un genere così specifico durante un periodo di tempo in cui gli stili architettonici e le tendenze hanno subito stravolgimenti ed evoluzioni che ancora oggi trovano una difficile connotazione e definizione precisa. L’analisi dell’architettura delle centrali idroelettriche, effettuata ripercorrendo le principali vicende del settore idroelettrico dalla fine del secolo scorso al secondo dopoguerra, oltre a considerare il rapporto con il contesto territoriale e culturale del nostro Paese vuole prendere in considerazione anche il particolare rapporto che in più casi si è venuto a creare tra committenti e progettisti. Compito della tesi è rileggere un settore poco indagato finora e capire se vi sia stata effettivamente una evoluzione architettonica dal punto di vista tipologico o se la centrale sia stata sempre affrontata come semplice esercizio di “vestizione” di un involucro precostituito da precise esigenze tecniche. La ricerca infatti si pone come obiettivo lo studio delle centrali non solo dal punto di vista tipologico e spaziale dei suoi principali elementi, ma si pone come obiettivo anche lo studio della loro distribuzione nel sito in cui sono sorte, distribuzione che spesso ha portato alla formazione di una sorta di vera e propria “città elettrica”, in cui la composizione dei vari elementi segue una logica compositiva ben precisa. Dal punto di vista del contributo originale la ricerca vuole proporre una serie di riflessioni ed elaborati inerenti alcune centrali non ancora indagate. Nel caso specifico di Portaluppi l’apporto originale consiste nell’aver portato alla luce notizie inerenti centrali che sono sempre state poste in secondo piano rispetto le ben più note e studiate centrali della Val d’Ossola. Nel caso invece di Muzio il contributo consiste in una analisi approfondita e in una comparazione di documenti che di solito sono sempre stati pubblicati come semplice apparato iconografico, ma che messi a confronto danno una lettura di quelle che sono state le fasi e le elaborazioni progettuali apportate dall’autore. Il tema della ricerca è stato affrontato poi attraverso una lettura delle fonti dirette relative agli scritti degli autori, con una contemporanea lettura di testi, articoli e interventi tratti dalle riviste appartenenti al periodo in esame per comprendere al meglio il panorama culturale e architettonico che hanno fatto da scenario alle esperienze di entrambe le figure oggetto di studio. Infine la ricerca si è concentrata sull’analisi di alcune opere in particolare - due centrali idroelettriche per ciascun autore oggetto della tesi - scelte perché considerate rappresentative sia per impianto spaziale e tipologico, sia per le scelte compositive e stilistiche adottate. La lettura dei manufatti architettonici scelti è stata condotta con l’analisi di copie di elaborati grafici originali, foto d’epoca e altri documenti reperiti grazie ad una ricerca condotta in vari archivi. Le centrali scelte nell’ambito delle esperienze maturate da Muzio e Portaluppi sono state individuate per rappresentare il quadro relativo allo sviluppo e alla ricerca di un nuovo linguaggio formale da adottare nell’ambito dell’architettura di questi manufatti. Per entrambi i protagonisti oggetto della ricerca sono state individuate due centrali in grado di dare una visione il più possibile completa dell’evoluzione della tematica delle centrali idroelettriche all’interno della loro esperienza, prendendo in considerazione soprattutto gli aspetti legati all’evoluzione del loro linguaggio compositivo e stilistico. L’individuazione delle centrali da analizzare è stata dettata prendendo in considerazione alcuni fattori come il tipo di impianto, le relazioni e confronto con il contesto geografico e naturale e le soluzioni adottate.

Expressiveness in biologically inspired languages

A very recent and exciting new area of research is the application of Concurrency Theory tools to formalize and analyze biological systems and one of the most promising approach comes from the process algebras (process calculi). A process calculus is a formal language that allows to describe concurrent systems and comes with well-established techniques for quantitative and qualitative analysis. Biological systems can be regarded as concurrent systems and therefore modeled by means of process calculi. In this thesis we focus on the process calculi approach to the modeling of biological systems and investigate, mostly from a theoretical point of view, several promising bio-inspired formalisms: Brane Calculi and k-calculus family. We provide several expressiveness results mostly by means of comparisons between calculi. We provide a lower bound to the computational power of the non Turing complete MDB Brane Calculi by showing an encoding of a simple P-System into MDB. We address the issue of local implementation within the k-calculus family: whether n-way rewrites can be simulated by binary interactions only. A solution introducing divergence is provided and we prove a deterministic solution preserving the termination property is not possible. We use the symmetric leader election problem to test synchronization capabilities within the k-calculus family. Several fragments of the original k-calculus are considered and we prove an impossibility result about encoding n-way synchronization into (n-1)-way synchronization. A similar impossibility result is obtained in a pure computer science context. We introduce CCSn, an extension of CCS with multiple input prefixes and show, using the dining philosophers problem, that there is no reasonable encoding of CCS(n+1) into CCSn.

Simulating Cortical Development as a Self Constructing Process: A Novel Multi-Scale Approach Combining Molecular and Physical Aspects

Current models of embryological development focus on intracellular processes such as gene expression and protein networks, rather than on the complex relationship between subcellular processes and the collective cellular organization these processes support. We have explored this collective behavior in the context of neocortical development, by modeling the expansion of a small number of progenitor cells into a laminated cortex with layer and cell type specific projections. The developmental process is steered by a formal language analogous to genomic instructions, and takes place in a physically realistic three-dimensional environment. A common genome inserted into individual cells control their individual behaviors, and thereby gives rise to collective developmental sequences in a biologically plausible manner. The simulation begins with a single progenitor cell containing the artificial genome. This progenitor then gives rise through a lineage of offspring to distinct populations of neuronal precursors that migrate to form the cortical laminae. The precursors differentiate by extending dendrites and axons, which reproduce the experimentally determined branching patterns of a number of different neuronal cell types observed in the cat visual cortex. This result is the first comprehensive demonstration of the principles of self-construction whereby the cortical architecture develops. In addition, our model makes several testable predictions concerning cell migration and branching mechanisms.

Método para el análisis independiente de problemas

habilidades de comprensión y resolución de problemas. Tanto es así que se puede afirmar con rotundidad que no existe el método perfecto para cada una de las etapas de desarrollo y tampoco existe el modelo de ciclo de vida perfecto: cada nuevo problema que se plantea es diferente a los anteriores en algún aspecto y esto hace que técnicas que funcionaron en proyectos anteriores fracasen en los proyectos nuevos. Por ello actualmente se realiza un planteamiento integrador que pretende utilizar en cada caso las técnicas, métodos y herramientas más acordes con las características del problema planteado al ingeniero. Bajo este punto de vista se plantean nuevos problemas. En primer lugar está la selección de enfoques de desarrollo. Si no existe el mejor enfoque, ¿cómo se hace para elegir el más adecuado de entre el conjunto de los existentes? Un segundo problema estriba en la relación entre las etapas de análisis y diseño. En este sentido existen dos grandes riesgos. Por un lado, se puede hacer un análisis del problema demasiado superficial, con lo que se produce una excesiva distancia entre el análisis y el diseño que muchas veces imposibilita el paso de uno a otro. Por otro lado, se puede optar por un análisis en términos del diseño que provoca que no cumpla su objetivo de centrarse en el problema, sino que se convierte en una primera versión de la solución, lo que se conoce como diseño preliminar. Como consecuencia de lo anterior surge el dilema del análisis, que puede plantearse como sigue: para cada problema planteado hay que elegir las técnicas más adecuadas, lo que requiere que se conozcan las características del problema. Para ello, a su vez, se debe analizar el problema, eligiendo una técnica antes de conocerlo. Si la técnica utiliza términos de diseño entonces se ha precondicionado el paradigma de solución y es posible que no sea el más adecuado para resolver el problema. En último lugar están las barreras pragmáticas que frenan la expansión del uso de métodos con base formal, dificultando su aplicación en la práctica cotidiana. Teniendo en cuenta todos los problemas planteados, se requieren métodos de análisis del problema que cumplan una serie de objetivos, el primero de los cuales es la necesidad de una base formal, con el fin de evitar la ambigüedad y permitir verificar la corrección de los modelos generados. Un segundo objetivo es la independencia de diseño: se deben utilizar términos que no tengan reflejo directo en el diseño, para que permitan centrarse en las características del problema. Además los métodos deben permitir analizar problemas de cualquier tipo: algorítmicos, de soporte a la decisión o basados en el conocimiento, entre otros. En siguiente lugar están los objetivos relacionados con aspectos pragmáticos. Por un lado deben incorporar una notación textual formal pero no matemática, de forma que se facilite su validación y comprensión por personas sin conocimientos matemáticos profundos pero al mismo tiempo sea lo suficientemente rigurosa para facilitar su verificación. Por otro lado, se requiere una notación gráfica complementaria para representar los modelos, de forma que puedan ser comprendidos y validados cómodamente por parte de los clientes y usuarios. Esta tesis doctoral presenta SETCM, un método de análisis que cumple estos objetivos. Para ello se han definido todos los elementos que forman los modelos de análisis usando una terminología independiente de paradigmas de diseño y se han formalizado dichas definiciones usando los elementos fundamentales de la teoría de conjuntos: elementos, conjuntos y relaciones entre conjuntos. Por otro lado se ha definido un lenguaje formal para representar los elementos de los modelos de análisis – evitando en lo posible el uso de notaciones matemáticas – complementado con una notación gráfica que permite representar de forma visual las partes más relevantes de los modelos. El método propuesto ha sido sometido a una intensa fase de experimentación, durante la que fue aplicado a 13 casos de estudio, todos ellos proyectos reales que han concluido en productos transferidos a entidades públicas o privadas. Durante la experimentación se ha evaluado la adecuación de SETCM para el análisis de problemas de distinto tamaño y en sistemas cuyo diseño final usaba paradigmas diferentes e incluso paradigmas mixtos. También se ha evaluado su uso por analistas con distinto nivel de experiencia – noveles, intermedios o expertos – analizando en todos los casos la curva de aprendizaje, con el fin de averiguar si es fácil de aprender su uso, independientemente de si se conoce o no alguna otra técnica de análisis. Por otro lado se ha estudiado la capacidad de ampliación de modelos generados con SETCM, para comprobar si permite abordar proyectos realizados en varias fases, en los que el análisis de una fase consista en ampliar el análisis de la fase anterior. En resumidas cuentas, se ha tratado de evaluar la capacidad de integración de SETCM en una organización como la técnica de análisis preferida para el desarrollo de software. Los resultados obtenidos tras esta experimentación han sido muy positivos, habiéndose alcanzado un alto grado de cumplimiento de todos los objetivos planteados al definir el método.---ABSTRACT---Software development is an inherently complex activity, which requires specific abilities of problem comprehension and solving. It is so difficult that it can even be said that there is no perfect method for each of the development stages and that there is no perfect life cycle model: each new problem is different to the precedent ones in some respect and the techniques that worked in other problems can fail in the new ones. Given that situation, the current trend is to integrate different methods, tools and techniques, using the best suited for each situation. This trend, however, raises some new problems. The first one is the selection of development approaches. If there is no a manifestly single best approach, how does one go about choosing an approach from the array of available options? The second problem has to do with the relationship between the analysis and design phases. This relation can lead to two major risks. On one hand, the analysis could be too shallow and far away from the design, making it very difficult to perform the transition between them. On the other hand, the analysis could be expressed using design terminology, thus becoming more a kind of preliminary design than a model of the problem to be solved. In third place there is the analysis dilemma, which can be expressed as follows. The developer has to choose the most adequate techniques for each problem, and to make this decision it is necessary to know the most relevant properties of the problem. This implies that the developer has to analyse the problem, choosing an analysis method before really knowing the problem. If the chosen technique uses design terminology then the solution paradigm has been preconditioned and it is possible that, once the problem is well known, that paradigm wouldn’t be the chosen one. The last problem consists of some pragmatic barriers that limit the applicability of formal based methods, making it difficult to use them in current practice. In order to solve these problems there is a need for analysis methods that fulfil several goals. The first one is the need of a formal base, which prevents ambiguity and allows the verification of the analysis models. The second goal is design-independence: the analysis should use a terminology different from the design, to facilitate a real comprehension of the problem under study. In third place the analysis method should allow the developer to study different kinds of problems: algorithmic, decision-support, knowledge based, etc. Next there are two goals related to pragmatic aspects. Firstly, the methods should have a non mathematical but formal textual notation. This notation will allow people without deep mathematical knowledge to understand and validate the resulting models, without losing the needed rigour for verification. Secondly, the methods should have a complementary graphical notation to make more natural the understanding and validation of the relevant parts of the analysis. This Thesis proposes such a method, called SETCM. The elements conforming the analysis models have been defined using a terminology that is independent from design paradigms. Those terms have been then formalised using the main concepts of the set theory: elements, sets and correspondences between sets. In addition, a formal language has been created, which avoids the use of mathematical notations. Finally, a graphical notation has been defined, which can visually represent the most relevant elements of the models. The proposed method has been thoroughly tested during the experimentation phase. It has been used to perform the analysis of 13 actual projects, all of them resulting in transferred products. This experimentation allowed evaluating the adequacy of SETCM for the analysis of problems of varying size, whose final design used different paradigms and even mixed ones. The use of the method by people with different levels of expertise was also evaluated, along with the corresponding learning curve, in order to assess if the method is easy to learn, independently of previous knowledge on other analysis techniques. In addition, the expandability of the analysis models was evaluated, assessing if the technique was adequate for projects organised in incremental steps, in which the analysis of one step grows from the precedent models. The final goal was to assess if SETCM can be used inside an organisation as the preferred analysis method for software development. The obtained results have been very positive, as SETCM has obtained a high degree of fulfilment of the goals stated for the method.

Linguistic Systems and Knowledge of Reality

Linguistic systems are the human tools to understand reality. But is it possible to attain this reality? The reality that we perceive, is it just a fragmented reality of which we are part? In this paper the authors present is an attempt to address this question from an epistemological and philosophic linguistic point of view.

Saint Mathew Law and Bonini Paradox in Textual Theory of Complex Models

The mathematical models of the complex reality are texts belonging to a certain literature that is written in a semi-formal language, denominated L(MT) by the authors whose laws linguistic mathematics have been previously defined. This text possesses linguistic entropy that is the reflection of the physical entropy of the processes of real world that said text describes. Through the temperature of information defined by Mandelbrot, the authors begin a text-reality thermodynamic theory that drives to the existence of information attractors, or highly structured point, settling down a heterogeneity of the space text, the same one that of ontologic space, completing the well-known law of Saint Mathew, of the General Theory of Systems and formulated by Margalef saying: “To the one that has more he will be given, and to the one that doesn't have he will even be removed it little that it possesses.

Bilingualism and educational achievement:a study of young bilinguals in Birmingham schools and colleges

This study aimed firstly to investigate current patterns of language use amongst young bilinguals in Birmingham and secondly to examine the relationship between this language use and educational achievement. The research then focussed on various practices, customs and attitudes which would favour the attrition or survival of minority languages in the British situation. The data necessary to address this question was provided by a sample of three hundred and seventy-four 16-19 year olds, studying in Birmingham schools and colleges during the period 1987-1990 and drawn from the main linguistic minority communities in Birmingham. The research methods chosen were both quantitative and qualitative. The study found evidence of ethnolinguistic vitality amongst many of the linguistic minority communities in Birmingham: a number of practices and a range of attitudes indicate that linguistic diversity may continue and that a stable diglossic situation may develop in some instances, particularly where demographical and religious factors lead to closeness of association. Where language attrition is occurring it is often because of the move from a less prestigious minority language or dialect to a more prestigious minority language in addition to pressures from English. The educational experience of the sample indicates that literacy and formal language study are of key importance if personal bilingualism is to be experienced as an asset; high levels of oral proficiency in the L1 and L2 do not, on their own, necessarily correlate with positive educational benefit. The intervening variable associated with educational achievement appears to be the formal language learning process and literacy. A number of attitudes and practices, including the very close associations maintained with some of the countries of origin of the families, were seen to aid or hinder first language maintenance and second language acquisition.