39 research outputs found
Bridging formal models : an engineering perspective
No full textThe thesis presents different techniques that can be used to build formal behavioral models. If modal properties are formulated, the models can be subjected to verification techniques to determine whether a model possesses the desired properties. However many native environments do not facilitate tools or techniques to verify them. Hence, these models need to be transformed into other models that provide suitable techniques for a formal analysis. The transformations are classified into two engineering approaches, namely syntactically engineered models and semantically engineered models. Syntactically engineered models are constructed from input specifications without explicitly considering the semantics. Semantically engineered models are constructed from input specifications by explicitly considering the semantics. The syntactic engineering approach presents four dedicated modeling techniques that construct or disseminate verification results for formal models. The first modeling technique describes a way to create models from system descriptions that specify concurrent behavior. Here, we model three variations of a 2×2 switch, for which the models are subsequently compared to models created in the specification languages: TLA+, Bluespec, Statecharts, and ACP. The comparison validates that mCRL2 is a suitable specification language to model descriptions or specify the behavior for prototype systems. The second syntactic technique constructs an mCRL2 model from a software implementation that operates a printer for printing Printed Circuit Boards. The model is used to advise (other) software engineers on dangerous language constructs in the control software. Hence, the model is model checked for various safety properties. The implementation is modeled through an over-approximation on the behavior by abstracting from program variables, such that only interface calls between processes and non-deterministic choices in procedures remain. The third modeling technique describes a language transformation from the language Chi 2.0 language to the mCRL2 language. The purpose of the transformation is to facilitate model checking techniques to the discrete part of the Chi 2.0 language
Analytic Techniques for Business Modeling: Opportunities for Advance
No full textElectrical Engineering, Mathematics and Computer Scienc
Optimising the Design of a Steel Substructure for Offshore Wind Turbines in Deeper Waters
No full textIn the need for more green energy a prominent role is reserved for wind energy. Offshore wind energy in deeper waters capitalises on more efficient wind properties and increased public acceptance compared to onshore wind energy and wind farms close to shore. In the coming years the offshore wind market is expected to evolve rapidly, especially in the deeper water range of thirty to sixty meter. In a business case preceding to this study as first reference a jacket type substructure was designed for a 6 MW turbine in a water depth of sixty meter. The goal of this thesis is to reduce the cost of this reference design in total use of material and assembly. Also the transportation and installation of the substructure are taken in consideration. First a step back is taken to reconsider the structural concept of the reference design. Several substructure concepts, like tripods and straight-leg jackets, have passed the review and firstly qualitative weighed against primary criteria in a Multi Criteria Analysis and subsequently by FEM based in-place analysis. The outcome of the total substructure weight and natural frequency with respect to frequency of wave loading and turbine excitement determined the decision to further investigate a three-leg and four-leg battered jacket. Thereto a fatigue analysis was performed. The calculation method used at the original reference design to determine the total fatigue damage due to turbine and wave loading was proven to be too optimistic and therefore modified. In relation to the reference design several optimisations have been proposed, including applying a horizontal brace just above mudline level, applying double sided butt welds and adopting K-bracing instead of X-bracing. Here the four enclosed pictures can be placed. (number 1 upmost left, number 4 upmost right) Finally, four designs have been worked out; the reference design (without optimisations), an optimised four-leg jacket, four-leg jacket with k-braces and a three-leg jacket. The total assembling cost of each design is calculated by considering the handling time and the welding volume with corresponding welding time of each weld. Together with the material use the total fabrication cost is assessed. The jacket shall be transported offshore by a standard North Sea barge. The dimensions of this barge potentially enable the transportation of three four-leg jackets and four three-leg jackets. Depending on the wind farm location this may lead to reduction of one tug and transport barge case of the three-leg jacket. Further consequence of the three-leg jacket is that a foundation pile less needs to be driven. Thereto is the installation time of the three-leg jacket reduced, resulting in less installation cost. By combining fabrication, transport and installation cost it is possible to compute an overview for substructures cost in a complete wind farm. Final conclusion is that the fabrication cost are decisive compared to the installation and transport cost. The four-leg jacket with K-braces turns out to be the most inexpensive design, respectively followed by the thee-leg jacket, the optimised four-leg jacket and the reference design. It is expected that the four-leg jacket with K-braces brings total cost reduction of approximately nine percent compared to the reference design.Structural and Building EngineeringDesign and ConstructionCivil Engineering and Geoscience
Ontgrondingen benedenstrooms van samenvloeiingen
No full textNa een uitgebreide literatuurstudie is onderzoek verricht naar de mogelijke oorzaken voor het ontstaan en de instandhouding van ontgrondingen benedenstrooms van samenvloeiingen van rivieren. Drie mogelijke verklaringen zijn nader onderzocht. Allereerst de mogelijkheid dat het voorkomen van de ontgrondingen een zelfde oorzaak heeft als het voorkomen van soortgelijke ontgrondingen in buitenbochten van rivieren. Een samenvloeiing wordt aldus gezien als twee aanliggende buitenbochten. Verantwoordelijk voor deze gaten is de door Struiksma beschreven herverdeling van zand en water in een bocht. In het geval van de sterk vlechtende Jamuna is de geldigheid van deze theorie echter beperkt. Het kan niet aangetoond worden dat dit mechanisme verantwoordelijk is voor het optreden van de ontgrondingen. De locatie van de ontgronding ten opzichte van de bocht sluit uit dat de ontgrondingskuil eenvoudig het diepste punt in de bocht is. Dit diepste punt in een buitenbocht treedt op een beperkte afstand benedenstrooms van de plaats waar de bochtstraal het kleinst is op; deze minimum bochtstraal wordt ver voor de ontgronding aangetroffen. De mogelijke rol van de traagheid van de secundaire stroming is nog onduidelijk. Als tweede mogelijke verklaring is onderzocht op welke wijze en in welke mate een stroomsnelheidsverschil tussen de beide bovenstroomse rivierarmen de grootte van de fluctuerende component van de snelheid u' beinvloed. De toename van het sedimenttransport wordt toegeschreven aan de verhoging van deze fluctuerende grootheid. Het gebied waarbinnen het snelheidsverschil tussen de beide stromen enige invloed op u' heeft is echter te beperkt, om een ontgronding enkele honderden meters benedenstrooms te verklaren. Een derde mogelijke verklaring, waarin een parallel wordt getrokken met de situatie van botsende stralen, moet onwaarschijnlijk geacht worden. De drukverhoging ter plaatse van de samenvloeiing buigt de beide aanstromende armen af en zorgt ervoor dat de stromen niet botsen, maar geleidelijk samenvloeien. De beide laatstgenoemde verklaringen zijn gebaseerd op de veronderstelling dat vergroting van de turbulentie-intensiteit leidt tot een verhoging van de transportcapaciteit van de stroming. In een later stadium is door middel van een rekenvoorbeeld aangegeven dat deze verhoogde transportcapaciteit slechts zeer beperkte ontgrondingen veroorzaakt.Hydraulic EngineeringCivil Engineering and Geoscience
Verification of safety requirements for program code using data abstraction
No full textLarge systems in modern development consist of many concurrent processes. To prove safety properties formal modelling techniques are needed. When source code is the only available documentation for deriving the system’s behaviour, it is a difficult task to create a suitable model. Implementations of a system usually describe behaviour in too much detail for a formal verification. Therefore automated methods are needed that directly abstract from the implementation, but maintain enough information for a formal system analysis.
This paper describes and illustrates a method by which systems with a high degree of parallelism can be verified. The method consists of creating an over-approximation of the behaviour by abstracting from the values of program variables. The derived model, consisting of interface calls between processes, is checked for various safety properties with the mCRL2 tool set
Breadth-bounded model checking
No full textModel checking large concurrent systems is a difficult task, due to the infamous state space explosion problem. To combat this problem, a technique called Bounded Model Checking has been proposed.
This techniques relies on restricting the level of unfoldings of the transition relation of a given specification. This technique is quite effective for verifying requirements that are relatively close to the initial state of the system's behaviour. Unfortunately, this technique is not adequate for disproving requirements which occur at levels that are relatively deep within the system. In this paper, we study an alternative approach to BMC by restricting the breadth of the transition relation, based on a Highway simulation. This allows us to find violations to (1) properties that lurk deep in a specification, and (2) properties that require lengthy counterexamples. Our experiments show that the method is complementary to BMC, and is effective in many practical applications
