A low-power 8-b 1 3.5-MHz video CMOS ADC for visiophony ISDNapplications

A half-flash, subranging, 8-b, 13.5-MHz, video ADC (analog-to-digital converter) using overlapped architecture that combines the advantages of both flash and half-flash converters is described. Its conversion rate is that of a flash, without any multiplexing and with a low number of comparators. Its low power consumption and the small silicon area required for its implementation enable it to be integrated in mixed digital/analog circuits such as a video acquisition circuit devoted to visiophony applications. It has been manufactured using a CMOS 1-μm technology with two polysilicon and two metallization layers     

The influence of hydro‐climatic and anthropogenic effects on the long‐term variation of commercial fisheries in a large floodplain river

This study deals with the effects of climate fluctuations and anthropogenic impacts on fisheries of Paraná River over the last 100 years. It is the first attempt to appraise the influence of hydro‐climatic and anthropogenic variables on the population changes of the most important inland fisheries of Argentina. Datasets covering more than eight decades (1935–2016) of a number of frequent and abundant commercial species inhabiting the main channel as well as the large floodplain of Paraná River were used. Our results suggest that fish catches and structure changed over time. Long and short‐term changes and reductions were closely related to fluctuations of 18 hydro‐climatic variables. Positive effects on the ichthyofauna were recorded during humid periods (1930–1940 and 1970–2000), when the frequency of large spring–summer floods increased. An increase in anthropic impacts (accounted for with nine variables) were recorded during the last two decades. We highlight the usefulness of the approach to support the management of the resources, ensuring sustainability of commercial fish assemblages and the long‐term conservation of biodiversity in big rivers.     

Event-B patterns and their tool support

Event-B has given developers the opportunity to construct models of complex systems that are correct-by-construction. However, there is no systematic approach, especially in terms of reuse, which could help with the construction of these models. We introduce the notion of design patterns within the framework of Event-B to shorten this gap. Our approach preserves the correctness of the models, which is critical in formal methods and also reduces the proving effort. Within our approach, an Event-B design pattern is just another model devoted to the formalisation of a typical sub-problem. As a result, we can use patterns to construct a model which can subsequently be used as a pattern to construct a larger model. We also present the interaction between developers and the tool support within the associated RODIN Platform of Event-B. The approach has been applied successfully to some medium-size industrial case studies.     

Aircraft landing gear system: approaches with Event-B to the modeling of an industrial system

International Journal on Software Tools for Technology Transfer - This paper describes the modeling, done using the Event-B notation, of the aircraft landing gear case study that was proposed in a...     

Rodin: an open toolset for modelling and reasoning in Event-B

Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. In this article we present the Rodin modelling tool that seamlessly integrates modelling and proving. We outline how the Event-B language was designed to facilitate proof and how the tool has been designed to support changes to models while minimising the impact of changes on existing proofs. We outline the important features of the prover architecture and explain how well-definedness is treated. The tool is extensible and configurable so that it can be adapted more easily to different application domains and development methods.     

Developing topology discovery in Event-B

We present a formal development in Event-B of a distributed topology discovery algorithm. Distributed topology discovery is at the core of several routing algorithms and is the problem of each node in a network discovering and maintaining information on the network topology. One of the key challenges in developing this algorithm is specifying the problem itself. We provide a specification that includes both safety properties, formalizing invariants that should hold in all system states, and liveness properties that characterize when the system reaches stable states. We prove these properties by appropriately combining proofs of invariants, event refinement, event convergence, and deadlock freedom. The combination of these features is novel and should be useful for formalizing and developing other kinds of semi-reactive systems, which are systems that react to, but do not modify, their environment. Our entire development has been formalized and machine checked using the Rodin tool.     

Faultless Systems: Yes We Can!

This paper presents simple ideas that offer suggestions on how to improve the situation of computerized system development. Gradually introducing some simple features will eventually result in a global improvement in the software development.     

A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol

The IEEE 1394 tree identify protocol illustrates the adequacy of the event-driven approach used together with the B Method. This approach provides a complete framework for developing mathematical models of distributed algorithms. A specific development is made of a series of more and more refined models. Each model is made of a number of static properties (the invariant) and dynamic parts (the guarded events). The internal consistency of each model as well as its correctness with regard to its previous abstraction are proved with the proof engine of Atelier B, which is the tool associated with B. In the case of IEEE 1394 tree identify protocol, the initial model is very primitive: it provides the basic properties of the graph (symmetry, acyclicity, connectivity), and its dynamic parts essentially contain a single event which elects the leader in one shot. Further refinements introduce more events, showing how each node of the graph non-deterministically participates in the leader election. At some stage in the development, message passing is introduced. This raises a specific potential contention problem, whose solution is given. The last stage of the refinement completely localises the events by making them take decisions based on local data only. Received July 2001/Accepted in revised form October 2003 Correspondence and offprint requests to: Dominique Méry, Université Henri Poincaré Nancy 1, LORIA, BP239, 54506 Vandœuvre-lès-Nancy Cedex, France. Email: mery@loria.fr     

The mathematical construction of a program

This paper is an exercise in program construction using Mathematics as a tool. The program which we undertake the construction of is a General Purpose Proof Checker. It is ‘general purpose’ in that it may take as input the axiomatization of a formal theory together with a proof written with this theory. As output it delivers a result which tells us whether the proof is correct or not.In order to test the generality of the proposed approach, we use the Proof Checker to check proofs written within theories such as Propositional Calculus and Predicate Calculus and Set Theory.