1,721 research outputs found
Applying Atomicity and Model Decomposition to a Space Craft System in Event-B
No full textEvent-B is a formal method for modeling and verifying consistency of systems. In formal methods such as Event-B, refinement is the process of enriching or modifying an abstract model in a step-wise manner in order to manage the development of complex and large systems. To further alleviate the complexity of developing large systems, Event-B refinement can be augmented with two techniques, namely atomicity decomposition and model decomposition. Our main objective in this paper is to investigate and evaluate the application of these techniques when used in a refinement based development. These techniques have been applied to the formal development of a space craft system. The outcomes of this experimental work are presented as assessment results. The experience and assessment can form the basis for some guidelines in applying these techniques in future cases
Shared Event Composition/Decomposition in Event-B
No full textThe construction of specifications is often a combination of smaller sub-components. Composition and decomposition are techniques that support reuse and allow us to formally combine sub-components through refinement steps while reusing their properties. Sub-components can result from a design or architectural goal and a refinement framework should allow further parallel development over the sub-components. We propose the definition of composition and decomposition in the Event-B formalism following a shared event approach where sub-components interact via synchronisation over shared events and shared states are not allow. We define the necessary proof obligations to ensure a valid composition or decomposition. We also show that shared event composition preserves refinement proofs for sub-components, that is, in order to maintain refinement of compositions, it is sufficient to prove refinement between corresponding subcomponents. A case study applying these two techniques is illustrated using Rodin, the Event-B toolset
Decomposition Structures for Event-B
No full textAbstract. Event-B provides a flexible approach to modelling and re-finement of systems. In this paper we outline two important ways in which Event-B refinement can be augmented with additional structuring to support further the management of complex refinements. Firstly we show how event refinement diagrams can be used to structure refinement steps involving decomposition of atomicity. Secondly we outline a tech-nique for decomposing models into sub-models to allow for independent refinement. We show how these two structuring techniques can be used together.
The Rodin Formal Modelling Tool
No full textWe present a software tool, the Rodin tool, for formal modelling in Event-B. Event-B is a notation and method developed from the B-Method and is intended to be used with an incremental style of modelling. The idea of incremental modelling has been taken from programming: modern programming languages come with integrated development environments that make it easy to modify and improve programs. The Rodin tool provides such an environment for Event-B. The two main characteristics of the Rodin tool are its ease of use and its extensibility. The tool focuses on modelling. It is easy to modify models and try out variations of a model. The tool can also be extended easily. This will make it possible to adapt the tool specific needs. So the tool can be adapted to fit into existing development processes instead demanding the opposite. We believe that these two characteristics are major points for industrial uptake
Supporting reuse mechanisms for developments in event-b: composition
No full textThe development of specifications often is a combination of smaller sub-components. Focusing on reuse, an interesting perspective is to formally define the combination of sub-components through refinement steps, reusing their properties and generating larger systems. The previous situation suggests the application of a reuse mechanism: composition. Event-B is a formal method that allows modelling and refinement of systems. The combination and reuse of existing sub-components is not currently supported in Event-B. We propose the development of composition by extending the Event-B formalism as an option for developing larger models, focusing in distributed systems. A tool is developed to support the shared event composition in the Rodin platform. Properties and proof obligations of sub-components are reused and sufficient proof obligations are generated to ensure valid composed models
Characterization and structure in the development of Tudor comedy
Get PDFThe role of characterization in dramatic structure is assessed by theoretical criteria.
Characters who perform actions necessary for the completion of the narrative sequence are
said to be "bound" to the narrative; those without such obligations are "free". Characters
who maintain a single, constant meaning during the course of a play are said to be "static";
characters who change or develop into new roles are "dynamic". Horatian decorum
demanded that comic characters be static, and the characters of Plautine and Terentian
tradition were almost always bound to narrative intrigue. However, evaluations of six
Tudor comedies show an increasing use of non-classical characterization within the comic
form.
In the early comedies lohan lohan and Roister Doister all characters are bound and
static, yet the impetus to enlarge the role of characterization is evident. The characters of
lohan lohan are expanded from their French source, and Roister Doister includes
extraneous episodes in which Udall displays his braggart hero. Free characters abound in
Misogonus; as well the play brings dynamic characterization into the scope of comedy with
the conversion of its prodigal son.
Free characters offer new possibilities of non-narrative plotting. In comedies of the
1580s favourite traditional characters appear as diversions outside the action, and thematic
arrangements of characters inform the increasingly complex plots. Lyly stresses the
symbolic potential of characters in Endimion, whereas Greene uses dynamic
characterization to heighten the illusion of independent figures in Friar Bacon and Friar
Bungay. Love's Labour's Lost exposes the limitations of comic artifice by pulling the
characters between convention and individualization.
By the end of the sixteenth century free and dynamic characters had become
common, and characterization had established a sizable claim on the design of English
comedy. These developments set the English form apart from its neoclassical counterparts
The Soldier's Marching Song
No full text(Color) Printed in blue, this postcard depicts two flags (Great Britain and the Royal Standard) and a crown with the words "Keep the Flag Flying." As per the title, the text can be sung to the tune of "Ring the Bell, Watchman" and the lyrics are written by Ralph W. Phipps specifically as a war song. This card is uninscribed and unposted
A Political Companion to Ralph Waldo Emerson
No full textFrom before the Civil War until his death in 1882, Ralph Waldo Emerson was renowned—and renounced—as one of the United States’ most prominent abolitionists and as a leading visionary of the nation’s liberal democratic future. Following his death, however, both Emerson’s political activism and his political thought faded from public memory, replaced by the myth of the genteel man of letters and the detached sage of individualism. In the 1990s, scholars rediscovered Emerson’s antislavery writings and began reviving his legacy as a political activist. A Political Companion to Ralph Waldo Emerson is the first collection to evaluate Emerson’s political thought in light of his recently rediscovered political activism.
What were Emerson’s politics? A Political Companion to Ralph Waldo Emerson authoritatively answers this question with seminal essays by some of the most prominent thinkers ever to write about Emerson—Stanley Cavell, George Kateb, Judith N. Shklar, and Wilson Carey McWilliams—as well as many of today’s leading Emerson scholars. With an introduction that effectively destroys the “pernicious myth about Emerson’s apolitical individualism” by editors Alan M. Levine and Daniel S. Malachuk, this volume reassesses Emerson’s famous theory of self-reliance in light of his antislavery politics, demonstrates the importance of transcendentalism to his politics, and explores the enduring significance of his thought for liberal democracy.
Including a substantial bibliography of work on Emerson’s politics over the last century, A Political Companion to Ralph Waldo Emerson is an indispensable resource for students of Emerson, American literature, and American political thought, as well as for those who wrestle with the fundamental challenges of democracy and liberalism.
Alan M. Levine, associate professor of political theory at American University, is the author of Sensual Philosophy: Toleration, Skepticism, and Montaigne’s Politics of the Self.
Daniel S. Malachuk, associate professor of English at Western Illinois University, is the author of Perfection, the State, and Victorian Liberalism.
This volume will quickly become indispensible for anyone writing about Emerson as a political thinker. -- Alex Zakaras, author of Mass Democracy: Mill, Emerson, and the Burdens of Citizenship
An important and timely corrective to the political inheritance of Emerson’s thinking—especially to the long-standing ‘pernicious myth’ of Emerson’s apolitical individualism. This collection demonstrates how Emerson is, and always has been, essential to our understanding and theorizing of American politics. -- David LaRocca, author of On Emerson and editor of Emerson’s Transcendental Etudes
A pathbreaking set of essays on the politics of Emerson. . . . Highly recommended. -- Choice
Makes a compelling case for reassessing Emerson\u27s political thought. -- Colloquyhttps://uknowledge.uky.edu/upk_english_language_and_literature_north_america/1072/thumbnail.jp
Performance Analysis of Probabilistic Action Systems
No full textFormal notations like B or action systems support a notion of refinement. Refinement relates an abstract specification A to a concrete specification C that is as least as deterministic. Knowing A and C one proves that C refines, or implements, specification A. In this study we consider specification A as given and concern ourselves with a way to find a good candidate for implementation C. To this end we classify all implementations of an abstract specification according to their performance. We distinguish performance from correctness. Concrete systems that do not meet the abstract specification correctly are excluded. Only the remaining correct implementations C are considered with respect to their performance. A good implementation of a specification is identified by having some optimal behaviour in common with it. In other words, a good refinement corresponds to a reduction of non-optimal behaviour. This also means that the abstract specification sets a boundary for the performance of any implementation. We introduce the probabilistic action system formalism which combines refinement with performance. In our current study we measure performance in terms of long-run expected average-cost. Performance is expressed by means of probability and expected costs. Probability is needed to express uncertainty present in physical environments. Expected costs express physical or abstract quantities that describe a system. They encode the performance objective. The behaviour of probabilistic action systems is described by traces of expected costs. A corresponding notion of refinement and simulation-based proof rules are introduced. Probabilistic action systems are based on discrete-time Markov decision processes. Numerical methods solving the optimisation problems posed by Markov decision processes are well-known, and used in a software tool that we have developed. The tool computes an optimal behaviour of a specification A thus assisting in the search for a good implementation C
- …
