Robo1 regulates the development of major axon tracts and interneuron migration in the forebrain

The Slit genes encode secreted ligands that regulate axon branching, commissural axon pathfinding and neuronal migration. The principal identified receptor for Slit is Robo ( Roundabout in Drosophila). To investigate Slit signalling in forebrain development, we generated Robo1 knockout mice by targeted deletion of exon 5 of the Robo1 gene. Homozygote knockout mice died at birth, but prenatally displayed major defects in axon pathfinding and cortical interneuron migration. Axon pathfinding defects included dysgenesis of the corpus callosum and hippocampal commissure, and abnormalities in corticothalamic and thalamocortical targeting. Slit2 and Slit1/2 double mutants display malformations in callosal development, and in corticothalamic and thalamocortical targeting, as well as optic tract defects. In these animals, corticothalamic axons form large fasciculated bundles that aberrantly cross the midline at the level of the hippocampal and anterior commissures, and more caudally at the medial preoptic area. Such phenotypes of corticothalamic targeting were not observed in Robo1 knockout mice but, instead, both corticothalamic and thalamocortical axons aberrantly arrived at their respective targets at least 1 day earlier than controls. By contrast, in Slit mutants, fewer thalamic axons actually arrive in the cortex during development. Finally, significantly more interneurons ( up to twice as many at E12.5 and E15.5) migrated into the cortex of Robo1 knockout mice, particularly in both rostral and parietal regions, but not caudal cortex. These results indicate that Robo1 mutants have distinct phenotypes, some of which are different from those described in Slit mutants, suggesting that additional ligands, receptors or receptor partners are likely to be involved in Slit/Robo signalling.

Molecular control of cell type diversity in the developing spinal cord

1, During embryonic development, a diverse array of neurons and glia are generated at specific positions along the dorsoventral and rostro-caudal axes of the spinal cord from a common pool of precursor cells. 2. This cell type diversity can be distinguished by the spatially and temporally coordinated expression of several transcription factors that are also linked to cell type specification at a very early stage of spinal cord development. 3, Recent studies have started to uncover that the generation of cell type diversity in the developing spinal cord. Moreover, distinct cell types in the spinal cord appear to be determined by the spatially and temporally coordinated expression of transcription factors. 4. The expression of these factors also appears to be controlled by gradients of factors expressed by ventral and dorsal midline cells, namely Sonic hedgehog and members of the transforming growth factor-beta family. 5, Changes in the competence of precursor cells and local cell interactions may also play important roles in cell type specification within the developing spinal cord.

Integrating formal specification and software verification and validation

It is not surprising that students are unconvinced about the benefits of formal methods if we do not show them how these methods can be integrated with other activities in the software lifecycle. In this paper, we describe an approach to integrating formal specification with more traditional verification and validation techniques in a course that teaches formal specification and specification-based testing. This is accomplished through a series of assignments on a single software component that involves specifying the component in Object-Z, validating that specification using inspection and a specification animation tool, and then testing an implementation of the specification using test cases derived from the formal specification.

A case study in specification and implementation testing

Achieving consistency between a specification and its implementation is an important part of software development In previous work, we have presented a method and tool support for testing a formal specification using animation and then verifying an implementation of that specification. The method is based on a testgraph, which provides a partial model of the application under test. The testgraph is used in combination with an animator to generate test sequences for testing the formal specification. The same testgraph is used during testing to execute those same sequences on the implementation and to ensure that the implementation conforms to the specification. So far, the method and its tool support have been applied to software components that can be accessed through an application programmer interface (API). In this paper, we use an industrially-based case study to discuss the problems associated with applying the method to a software system with a graphical user interface (GUI). In particular, the lack of a standardised interface, as well as controllability and observability problems, make it difficult to automate the testing of the implementation. The method can still be applied, but the amount of testing that can be carried on the implementation is limited by the manual effort involved.

Partial completion of activity in business process specification

We examine the current workflow modelling capability from a new angle and demonstrate a weakness of current workflow specification languages in relation to execution of activities. This shortcoming is mainly due to serious limitations of the corresponding computational/execution model behind the business process modelling language constructs. The main purpose of this paper is the introduction of new specification/modelling constructs allowing for more precise representation of complex activity states during its execution. This new concept enables visibility of a new activity state–partial completion of activity, which in turn allows for a more flexible and precise enforcement/monitoring of automated business processes.

A graphical specification of model transformations with triple graph grammars

Models and model transformations are the core concepts of OMG's MDA (TM) approach. Within this approach, most models are derived from the MOF and have a graph-based nature. In contrast, most of the current model transformations are specified textually. To enable a graphical specification of model transformation rules, this paper proposes to use triple graph grammars as declarative specification formalism. These triple graph grammars can be specified within the FUJABA tool and we argue that these rules can be more easily specified and they become more understandable and maintainable. To show the practicability of our approach, we present how to generate Tefkat rules from triple graph grammar rules, which helps to integrate triple graph grammars with a state of a art model transformation tool and shows the expressiveness of the concept.

Pockets of flexibility in workflow specification

Workflow technology is currently being deployed in quite diverse domains. However, the element of change is present in some degree and form in almost all domains. A workflow implementation that does not support the process of change will not benefit the organization in the long run. Change can be manifested in different forms in workflow processes. In this paper, we first present a categorization of workflow change characteristics and divide workflow processes into dynamic, adaptive and flexible processes. We define flexibility as the ability of the workflow process to execute on the basis of a loosely, or partially specified model, where the full specification of the model is made at runtime, and may be unique to each instance. To provide a modeling framework that offers true flexibility, we need to consider the factors, which influence the paths of (unique) instances together with the process definition. We advocate an approach that aims at making the process of change part of the workflow process itself. We introduce the notion of an open instance that consists of a core process and several pockets of flexibility, and present a framework based on this notion, which makes use of special build activities that provide the functionality to integrate the process of defining a change, into the open workflow instance.

Abstract specification in Object-Z and CSP

A number of integrations of the state-based specification language Object-Z and the process algebra CSP have been proposed in recent years. In developing such integrations, a number of semantic decisions have to be made. In particular, what happens when an operation's precondition is not satisfied? Is the operation blocked, i.e., prevented from occurring, or can it occur with an undefined result? Also, are outputs from operations angelic, satisfying the environment's constraints on them, or are they demonic and not influenced by the environment at all? In this paper we discuss the differences between the models, and show that by adopting a blocking model of preconditions together with an angelic model of outputs one can specify systems at higher levels of abstraction.

Determining the specification of a control system from that of its environment

Well understood methods exist for developing programs from given specifications. A formal method identifies proof obligations at each development step: if all such proof obligations are discharged, a precisely defined class of errors can be excluded from the final program. For a class of closed systems such methods offer a gold standard against which less formal approaches can be measured. For open systems -those which interact with the physical world- the task of obtaining the program specification can be as challenging as the task of deriving the program. And, when a system of this class must tolerate certain kinds of unreliability in the physical world, it is still more challenging to reach confidence that the specification obtained is adequate. We argue that widening the notion of software development to include specifying the behaviour of the relevant parts of the physical world gives a way to derive the specification of a control system and also to record precisely the assumptions being made about the world outside the computer.

Supporting the software testing process through specification animation

Achieving consistency between a specification and its implementation is an important part of software development. In this paper, we present a method for generating passive test oracles that act as self-checking implementations. The implementation is verified using an animation tool to check that the behavior of the implementation matches the behavior of the specification. We discuss how to integrate this method into a framework developed for systematically animating specifications, which means a tester can significantly reduce testing time and effort by reusing work products from the animation. One such work product is a testgraph: a directed graph that partially models the states and transitions of the specification. Testgraphs are used to generate sequences for animation, and during testing, to execute these same sequences on the implementation.