62 resultados para formal verification


Relevância:

20.00% 20.00%

Publicador:

Resumo:

We consider systems composed of a base system with multiple “features” or “controllers”, each of which independently advise the system on how to react to input events so as to conform to their individual specifications. We propose a methodology for developing such systems in a way that guarantees the “maximal” use of each feature. The methodology is based on the notion of “conflict-tolerant” features that are designed to continue offering advice even when their advice has been overridden in the past. We give a simple priority-based composition scheme for such features, which ensures that each feature is maximally utilized. We also provide a formal framework for specifying, verifying, and synthesizing such features. In particular we obtain a compositional technique for verifying systems developed in this framework.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

A theory and generalized synthesis procedure is advocated for the design of weir notches and orifice-notches having a base in any given shape, to a depth a, such that the discharge through it is proportional to any singular monotonically-increasing function of the depth of flow measured above a certain datum. The problem is reduced to finding an exact solution of a Volterra integral equation in Abel form. The maximization of the depth of the datum below the crest of the notch is investigated. Proof is given that for a weir notch made out of one continuous curve, and for a flow proportional to the mth power of the head, it is impossible to bring the datum lower than (2m − 1)a below the crest of the notch. A new concept of an orifice-notch, having discontinuity in the curve and a division of flow into two distinct portions, is presented. The division of flow is shown to have a beneficial effect in reducing the datum below (2m − 1)a from the crest of the weir and still maintaining the proportionality of the flow. Experimental proof with one such orifice-notch is found to have a constant coefficient of discharge of 0.625. The importance of this analysis in the design of grit chambers is emphasized.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

Enantioselective formal total syntheses of the marine trisnorsesquiterpenes clavukerin A and isoclavukerin A, starting from (R)-limonene employing an RCM reaction as the key step, are described.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

Two dimensional Optical Orthogonal Codes (OOCs) named Wavelength/Time Multiple-Pulses-per-Row (W/T MPR) codes suitable for use in incoherent fiber-optic code division multiple access (FO-CDMA) networks are reported in [6]. In this paper, we report the construction of W/T MPR codes, using Greedy Algorithm (GA), with distinct 1-D OOCs [1] as the row vectors. We present the W/T MPR codes obtained using the GA. Further, we verify the correlation properties of the generated W/T MPR codes using Matlab.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

A short but uneventful formal synthesis of perhydrogephyrotoxin 3 from readily available tricyclo[5.2.1.0(2,6)]decane derivative 8 via the intermediacy of the cis-hydroindanone 13 is reported. This work constitutes further demonstration of the carbocycle-heterocycle equivalency theme in the synthesis of alkaloids.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

General' objects, which are specially prepared to possess restricted spatial frequency spectra, have been used in the conventional Lau experiment to obtain experimental proof for the existence of lateral periodicity arising from axial periodicity, for a subclass of axially periodic wavefields in an incoherent situation.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

The enantiodivergent formal syntheses of both enantiomers of aspercyclide C is accomplished. Starting from L-(+)-tartaric acid, the key protected allylic alcohol, (3R,4R)-4-(methoxy-methoxy) non-1-en-3-ol is prepared, and is then elaborated into both enantiomers of 3-(4-methoxybenzyl)oxy]non-1-en-4-ol via Mitsunobu inversion. Esterification with a known biaryl acid, followed by ring-closing metathesis and deprotection completes the syntheses.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

A conformationally locked fluoropentol undergoes an interesting transformation to (trans,anti,trans,anti,trans)-perhydro-2,3,4a,6,7,8a-naphthalenehexol essentially under conditions of base-induced transesterification. The proposed rationale for the observed metamorphosis involves a nucleophilic displacement of fluoride, and subsequent stereo- and regioselective anti-Furst-Plattner-type ring-opening of the epoxide thus formed.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

The formal total synthesis of (+)-didemniserinolipid B, a marine tunicate possessing a 6,8-dioxabicyclo3.2.1]octane framework, was accomplished starting from L-(+)-tartaric acid. The key transformations in the synthesis include the elaboration of a gamma-hydroxy-amide readily obtained by desymmetrization of tartaric acid bis-amide via the controlled addition of a Grignard reagent followed by stereoselective reduction of the resulting ketone. (C) 2010 Elsevier Ltd. All rights reserved.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

A general and simple methodology for spirocyclopentannulation of cyclic ketones (or 4,4-disubstituted cyclopentenones from acyclic ketones) and its application in the synthesis of the spirodienone 7 via a prochiral precursor constituting a formal total synthesis of (+/-)-acorone (6), are described.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

Memory models of shared memory concurrent programs define the values a read of a shared memory location is allowed to see. Such memory models are typically weaker than the intuitive sequential consistency semantics to allow efficient execution. In this paper, we present WOMM (abbreviation for Weak Operational Memory Model) that formally unifies two sources of weak behavior in hardware memory models: reordering of instructions and weakly consistent memory. We show that a large number of optimizations are allowed by WOMM. We also show that WOMM is weaker than a number of hardware memory models. Consequently, if a program behaves correctly under WOMM, it will be correct with respect to those hardware memory models. Hence, WOMM can be used as a formally specified abstraction of the hardware memory models. Moreover; unlike most weak memory models, WOMM is described using operational semantics, making it easy to integrate into a model checker for concurrent programs. We further show that WOMM has an important property - it has sequential consistency semantics for datarace-free programs.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

ChemInform is a weekly Abstracting Service, delivering concise information at a glance that was extracted from about 100 leading journals. To access a ChemInform Abstract of an article which was published elsewhere, please select a “Full Text” option. The original article is trackable via the “References” option.

Relevância:

20.00% 20.00%

Publicador:

Resumo:

A new strategy for the construction of A-ring aromatic steroids which resulted in the formal total synthesis of estrone is described. Thus reaction of the adduct (9), obtained from 1-methoxy-4-methylcyclohexa-1,4-diene and acrolein, with 3-(m-methoxyphenyl)propylmagnesium bromide followed by oxidation afforded the bicyclo[2.2.2]octene derivative (14). Acid-catalysed rearrangement of (14) followed by an intramolecular Michael addition resulted in the cis tetraenone (18) which was dehydrogenated with palladium chloride to the pentaenone (22). Li/NH3 reduction of (22) gave 3-methoxy-D-homoestra-1,3,5(10)-trien-16-one (31) which has been converted into the methyl ether (37) of marrianolic acid, and its methyl ester (38).

Relevância:

20.00% 20.00%

Publicador:

Resumo:

A radical cyclization based methodology has been applied for the formal total synthesis of (+/-)-enterolactone (1), the first lignan isolated from human source. Bromoacetalization reaction of the cinnamyl alcohols 7 and 13 using ethyl vinyl ether and NBS, generated the bromoacetals 8 and 15. The 5-exo-trig radical cyclization reaction of the bromoacetals 8 and 15 with in situ generated catalytic tri-a-butyltin hydride and AIBN furnished a 3 : 2 diastereomeric mixture of the cyclic acetals 9 and 16. Sonochemically accelerated Jones oxidation of the cyclic acetals 9 and 16 yielded the gamma-butyrolactones 10 and 12 completing the formal total synthesis of (+/-)-enterolactone. Alternatively radical cyclization of the bromoacetate 17 furnished a 1 : 2 mixture of the lactone 10 and the reduced product 18.