Search

The verification of many practical systems - in particular, embedded systems - involves processes executing over time, for which it is common to use models based on temporal logic, in either its linear (LTL) or branching (CTL). Some of today’s most advanced automatic program verifiers, however, rely on non-temporal theories, particularly Hoare-style logic. Can we still take advantage of this sophisticated verification technology for more challenging systems? As a step towards a positive answer, we have defined a translation scheme from temporal specifications to contract-equipped object-oriented programs, expressed in Eiffel and hence open for processing by the AutoProof program prover. We have applied this scheme to a published CTL model of a widely used realistic example, the “landing gear” system which has been the subject of numerous competing specifications. An attempt to verify the result in AutoProof failed to prove one temporal property, which on further inspection seemed to be wrong in the original published model, even though the published work claimed to have verified an Abstract State Machine implementation of that model. Correcting the CTL specification to reflect the apparent informal attempt, re-translating again to contracted Eiffel and re-running the verification leads to success. The LTL-to-contracted-Eiffel process is still ad hoc, and tailored to generate the kind of scheme that the target verification tool (AutoProof) can handle best, rather than the simplest or most elegant scheme. Even with this limitation, the results highlight the need for rigor in the verification process, and (on the positive side) demonstrate that the highly advanced mechanized proof technology developed over several decades for the verification of traditional programs also has the potential of handling the demanding needs of embedded systems and other demanding contemporary developments.

The extent of formal verification methods applied to industrial projects has always been limited. The proliferation of distributed ledger systems (DLS), also known as blockchain, is rapidly changing the situation. Since the main area of DLSs' application is the automation of financial transactions, the properties of predictability and reliability are critical for implementing such systems. The actual behavior of the DLS is determined by the chosen consensus protocol, which properties require strict specification and formal verification. Formal specification and verification of the consensus protocol is necessary but not sufficient. It is required to ensure that the software implementation of the DLS nodes complies with this protocol. The verified software implementation of the protocol must run on a fairly reliable operating system. The so-called “smart contracts”, which are an important part of the applied implementations of specific business processes based on DLSs, must be verifiable as well. In this paper, we describe an ongoing industrial project that will result in a DLS verified at least at the four technological levels described above. We then share our experience with the formal specification and verification of HotStuff, a leader-based fault-tolerant protocol that ensures reaching distributed consensus in the presence of Byzantine processes.

Within the Terek-Caspian oil and gas bearing basin of the Eastern Ciscaucasia, oil deposits occur in a wide stratigraphic range of rocks of the Mesozoic-Cenozoic section, from the Jurassic, at depths from 5800 to 200 m. In the sedimentary section, carbonate and terrigenous Middle Jurassic, Lower Cretaceous, Oligocene-Lower Miocene and Miocene oil-mother rocks are distinguished. Organic matter from them have different geochemical characteristics and different maturity to realize the generation potential. The article presents the results of a comprehensive study of potential petroleum-bearing rocks and hydrocarbon fluids from the Terek-Sunzha folded zone of the Terek-Caspian Trough, including lithological, chemical-bituminological, pyrolytic, chromatographic and chromatographic-mass spectrometry investigations. A detailed description of hydrocarbon fluids at the molecular level and genetic correlations of oil-oil and oil-organic matter are given. Specific features of the oil deposits of the Mesozoic-Cenozoic section are noted. Among the studied bitumens, the chromatographic characteristics of the extractable organic matter from the Khadum carbonate-clayey deposits and oils from the Cretaceous and Neogene reservoirs are most similar. The composition of a complex natural mixture of hydrocarbons from various sources, with different maturation during the geological history of the region, does not allow making unambiguous conclusions about the source or sources of hydrocarbons for the deposits of the Terek-Caspian Trough.

One of the main modern aim for oil industry is the development of hydrocarbon extraction technologies from «oil shale». In Russia there are kerogen-saturated carbonate-clayey-siliceous deposits of the Bazhenov Formation, carbonate rocks of the Volga-Ural and Timan-Pechora oil and gas bearing basins and clayey Maikop series of Pre-Caucasus region. The Khadum Formation is lower part of the Maikop series represented by carbonate-clay and clayey deposits. On the basis of long-term field and laboratory investigation conducted by specialists of the Oil and Gas Department from Geological Faculty of the Lomonosov Moscow State University. a comprehensive study of the lithological composition, structure, geochemical, hydrogeological and hydrodynamic characteristics of the Paleogene section and monitoring of the drilled wells, the prospects of the oil and gas potential of the Khadum deposits of the Oligocene in the Eastern Pre-Caucasus oil and gas bearing basin were estimated. 11 gas and 19 oil deposits are discovered within the Khadum deposits, and they are confined to the sand layers and lenses, but most of the Khadum section belongs to «unconventional» sources of hydrocarbons. Based on the integrated approach, a map of oil and gas potential prospects for the Khadum deposits was constructed. Highly prospective territories for drilling for oil, areas with small and medium perspectives, and gas prospecting areas have been singled out. Recommendations are given for drilling and technology for the development of the Pre-Caucasus oil shales, based on the world experience in the development of such formations.

A major determinant of the quality of software systems is the quality of their requirements, which should be both understandable and precise. Most requirements are written in natural language, which is good for understandability but lacks precision. To make requirements precise, researchers have for years advocated the use of mathematics-based notations and methods, known as "formal." Many exist, differing in their style, scope, and applicability. The present survey discusses some of the main formal approaches and compares them to informal methods. The analysis uses a set of nine complementary criteria, such as level of abstraction, tool availability, and traceability support. It classifies the approaches into five categories based on their principal style for specifying requirements: natural-language, semi-formal, automata/graphs, mathematical, and seamless (programming-language-based). It includes examples from all of these categories, altogether 21 different approaches, including for example SysML, Relax, Eiffel, Event-B, and Alloy. The review discusses a number of open questions, including seamlessness, the role of tools and education, and how to make industrial applications benefit more from the contributions of formal approaches. [ABSTRACT FROM AUTHOR]

The junction zone of the Caspian syneclise, the Russian Plate and the Pre-Ural trough is characterized by a complex structure. It has been studied in some detail during large-scale geological, geophysical, and drilling operations in the search for mineral deposits. Subsalt deposits are associated with the main prospects for the growth of hydrocarbon reserves in this region. This makes it important to rethink the available data and conduct scientific analysis to identify patterns of formation of sedimentary complexes and an integrated assessment of their possible hydrocarbon productivity by means of sedimentation modeling. The structure and history of the formation of five large sedimentary complexes: the Ordovician-Lower Devonian, the Central Middle Devonian, the Frasnian-Tournaisian, the Visean-Upper Carboniferous, and the Permian are considered in detail. For each complex, a structural-formational position and sedimentation conditions are determined, which should determine the hydrocarbon productivity of local objects. The revealed relationship between the conditions of carbonate sediments accumulation and their potential reservoir properties served as the basis for forecasting the productivity of regional natural reservoirs. The paper presents a generalized model of the formation of subsalt strata and the forecast of the spatial distribution of different facies deposits, which play the role of accumulating and preserving strata. The results obtained are applicable in the practice of oil and gas exploration in the region

Requirements and code, in conventional software engineering wisdom, belong to entirely different worlds. Is it possible to unify these two worlds? A unified framework could help make software easier to change and reuse. To explore the feasibility of such an approach, the case study reported here takes a classic example from the requirements engineering literature and describes it using a programming language framework to express both domain and machine properties. The paper describes the solution, discusses its benefits and limitations, and assesses its scalability.