Anisotropy in injection-molded ethylene-propylene-diene rubbers. Part I

Anisotropy and molecular orientation are well-known phenomena in the field of thermoplastics. In the case of rubber materials only a few studies have described anisotropy. Injection molding has been shown to give rise to higher anisotropy than compression molding. The anisotropy in the rubber material is assumed to be due to molecular orientation and is strengthened by carbon black. In order to understand the mechanism of anisotropy in rubber materials, an extensive study has been performed. In this paper, results from two injection-molded ethylene-propylene-diene (EPDM) rubbers, compounded both with and without carbon black, are presented. The polymers had different molecular weight distributions and the compounds were injected into center-gated 1- and 4-mm-thick disks. The properties measured in different directions were mechanical, dynamic mechanical, and swelling. These measurements show that anisotropy can be a very important factor to take into account. The origin of anisotropy is presumably the molecular orientation which arises during the filling of the mold with the rubber melt.     

The design of an interactive program development system for Pascal

A program language can be defined as the language in which computer programs are written, and a programming language as the language used by the programmer to create programs. This paper presents the design of an interactive program development system which uses Pascal as both program and programming language. Principal properties of the system are a complete immediate syntax check, a program-structure oriented editor, incremental compiling techniques, and interactive interpretation and debugging of programs. The syntax check is split into three phases, and the user can change the degree of check wanted. After a change of the program only part of it is recompiled, and only necessary phases of the compiling process are performed.     

On correctness of information models

During the last decade a number of approaches to information modelling, or conceptual modelling, have been presented. In most approaches it is assumed that the correctness of an information model is decided from intuitive considerations, though formal methods may be applied.In this report we discuss three correctness criteria of information models, namely: consistency, satisfiability and completeness. The satisfiability of an information model in a universe of discourse can be formally checked by complementing the information model with a representation of concrete knowledge which is assumed to be complete. A formal basis for such correctness checking is presented. Further, the relationship between an information model and a conceptual schema is discussed, and an observed transformation problem is presented.     

Regular model checking for LTL(MSO)

Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. We present LTL(MSO), a combination of the logics monadic second-order logic (MSO) and LTL as a natural logic for expressing the temporal properties to be verified in regular model checking. In other words, LTL(MSO) is a natural specification language for both the system and the property under consideration. LTL(MSO) is a two-dimensional modal logic, where MSO is used for specifying properties of system states and transitions, and LTL is used for specifying temporal properties. In addition, the first-order quantification in MSO can be used to express properties parameterized on a position or process. We give a technique for model checking LTL(MSO), which is adapted from the automata-theoretic approach: a formula is translated to a buchi regular transition system with a regular set of accepting states, and regular model checking techniques are used to search for models. We have implemented the technique, and show its application to a number of parameterized algorithms from the literature.     

Using refinement calculus techniques to prove linearizability

Stepwise refinement is a method for systematically transforming a high-level program into an efficiently executable one. A sequence of successively refined programs can also serve as a correctness proof, which makes different mechanisms in the program explicit. We present rules for refinement of multi-threaded shared-variable concurrent programs. We apply our rules to the problem of verifying linearizability of concurrent objects, that are accessed by an unbounded number of concurrent threads. Linearizability is an established correctness criterion for concurrent objects, which states that the effect of each method execution can be considered to occur atomically at some point in time between its invocation and response. We show how linearizability can be expressed in terms of our refinement relation, and present rules for establishing this refinement relation between programs by a sequence of local transformations of method bodies. Contributions include strengthenings of previous techniques for atomicity refinement, as well as an absorption rule, which is particularly suitable for reasoning about concurrent algorithms that implement atomic operations. We illustrate the application of the refinement rules by proving linearizability of Treiber’s concurrent stack algorithm and Michael and Scott’s concurrent queue algorithm.     

Improving software security with static automated code analysis in an industry setting

Software security can be improved by identifying and correcting vulnerabilities. In order to reduce the cost of rework, vulnerabilities should be detected as early and efficiently as possible. Static automated code analysis is an approach for early detection. So far, only few empirical studies have been conducted in an industrial context to evaluate static automated code analysis. A case study was conducted to evaluate static code analysis in industry focusing on defect detection capability, deployment, and usage of static automated code analysis with a focus on software security. We identified that the tool was capable of detecting memory related vulnerabilities, but few vulnerabilities of other types. The deployment of the tool played an important role in its success as an early vulnerability detector, but also the developers perception of the tools merit. Classifying the warnings from the tool was harder for the developers than to correct them. The correction of false positives in some cases created new vulnerabilities in previously safe code. With regard to defect detection ability, we conclude that static code analysis is able to identify vulnerabilities in different categories. In terms of deployment, we conclude that the tool should be integrated with bug reporting systems, and developers need to share the responsibility for classifying and reporting warnings. With regard to tool usage by developers, we propose to use multiple persons (at least two) in classifying a warning. The same goes for making the decision of how to act based on the warning. Copyright © 2012 John Wiley & Sons, Ltd.     

A longitudinal study of VDT work and health

A longitudinal study on the use of visual display terminals (VDTs) was conducted with questionaire data obtained 1981 and in 1987–1988 from a cohort of office workers. The use of VDTs became more widespread in these offices during the intervening time period, but the time spent by individuals working at VDTs showed no general increase. The data suggested that VDT use was related to the risk of developing eye discomforts and hand and wrist problems. For skin problems and headache, risks for VDT and non‐VDT users were fairly similar, but indications of increased risks were found for certain groups and situations. The risks of developing neck, shoulder, shoulder joint, or upper arm problems were high for both VDT and non‐VDT users, but there were, in this study, no convincing suggestions that these risks were higher for VDT users compared to nonusers.     

Domain‐specific design of user interfaces

The use of graphical user interfaces in a computerized work environment is often considered to substantially improve the work situation. The outcome can, however, often be the opposite. Inappropriate use of windowing techniques, scrolling, and colors can result in tedious and confusing interaction with the computer. Today's standards and style guides define basic design principles but are insufficient for design of interfaces to end‐user applications. Here detailed domain knowledge is indeed essential. A domain‐specific style guide (DSSG) is an extension of today's standard with domain‐specific primitives, interface elements, and forms, together with domain‐specific guidelines. Careful dedicated analysis of information utilization in a domain is the development basis for a DSSG. The development is performed with an object‐oriented approach to facilitate the reuse of interface components and to support consistency and structure. Using a DSSG, the development of applications can be performed with a simplified information analysis. Therefore a more effective design process is possible, one in which end users can participate in the design using their own familiar domain‐related terminology. Time and costs for the development process can be drastically reduced if domain‐specific style guides, design guidelines, and development tools are used.     

Note: fast and reliable fracture strain extraction technique applied to silicon at nanometer scale

Simple fabrication process and extraction procedure to determine the fracture strain of monocrystalline silicon are demonstrated. Nanowires/nanoribbons in silicon are fabricated and subjected to uniaxial tensile stress along the complete length of the beams. Large strains up to 5% are measured for nanowires presenting a cross section of 50 nm × 50 nm and a length of 2.5 μm. An increase in fracture strain for silicon nanowires (NWs) with the downscaling of their volume is observed, highlighting the reduction of the defects probability as volume is decreased.     

Verifying Programs with Unreliable Channels

We consider the verification of a particular class of infinite-state systems, namely systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels. This class is able to model, e.g., link protocols such as the Alternating Bit Protocol and HDLC. For this class of systems, we show that several interesting verification problems are decidable by giving algorithms for verifying (1) thereachability problem—is a finite set of global states reachable from some other global state of the system ? (2)safety properties over tracesformulated as regular sets of allowed finite traces, and (3)eventuality properties—do all computations of a system eventually reach a given set of states? We have used the algorithms to verify some idealized sliding-window protocols with reasonable time and space resources. Our results should be contrasted with the well-known fact that these problems are undecidable for systems with unboundedperfectFIFO channels.