Complex communicating computer systems—computers connected by data networks and in constant communication with their environments—do not always behave as expected. This book introduces behavioral modeling, a rigorous approach to behavioral specification and verification of concurrent and distributed systems. It is among the very few techniques capable of modeling systems interaction at a level of abstraction sufficient for the interaction to be understood and analyzed.
Engineering education in the United States was long regarded as masculine territory. For decades, women who studied or worked in engineering were popularly perceived as oddities, outcasts, unfeminine (or inappropriately feminine in a male world). In Girls Coming to Tech!, Amy Bix tells the story of how women gained entrance to the traditionally male field of engineering in American higher education.
This book offers a general overview of the physics, concepts, theories, and models underlying the discipline of aerodynamics. A particular focus is the technique of velocity field representation and modeling via source and vorticity fields and via their sheet, filament, or point-singularity idealizations. These models provide an intuitive feel for aerodynamic flow-field behavior and are the basis of aerodynamic force analysis, drag decomposition, flow interference estimation, and other important applications. The models are applied to both low speed and high speed flows.
The technology of mechanized program verification can play a supporting role in many kinds of research projects in computer science, and related tools for formal proof-checking are seeing increasing adoption in mathematics and engineering. This book provides an introduction to the Coq software for writing and checking mathematical proofs. It takes a practical engineering focus throughout, emphasizing techniques that will help users to build, understand, and maintain large Coq developments and minimize the cost of code change over time.
Modern, complex digital systems invariably include hardware-implemented finite state machines. The correct design of such parts is crucial for attaining proper system performance. This book offers detailed, comprehensive coverage of the theory and design for any category of hardware-implemented finite state machines. It describes crucial design problems that lead to incorrect or far from optimal implementation and provides examples of finite state machines developed in both VHDL and SystemVerilog (the successor of Verilog) hardware description languages.
Engineering has been an essential collaborator in biological research and breakthroughs in biology are often enabled by technological advances. Decoding the double helix structure of DNA, for example, only became possible after significant advances in such technologies as X-ray diffraction and gel electrophoresis. Diagnosis and treatment of tuberculosis improved as new technologies—including the stethoscope, the microscope, and the X-ray—developed.
Climate engineering—which could slow the pace of global warming by injecting reflective particles into the upper atmosphere—has emerged in recent years as an extremely controversial technology. And for good reason: it carries unknown risks and it may undermine commitments to conserving energy. Some critics also view it as an immoral human breach of the natural world. The latter objection, David Keith argues in A Scientist’s Case for Climate Engineering, is groundless; we have been using technology to alter our environment for years.
Urbanization and globalization have shaped the last hundred years. These two dominant trends are mutually reinforcing: globalization links countries through the networked communications of urban hubs. The urban population now generates more than eighty percent of global GDP. Cities account for enormous flows of energy and materials—inflows of goods and services and outflows of waste. Thus urban environmental management critically affects global sustainability.
Human survival depends on a continuing supply of energy, but the need for ever-increasing amounts of it poses a dilemma: How can we find energy sources that are sustainable and ways to convert and utilize energy that are more efficient? This widely used textbook is designed for advanced undergraduate and graduate students as well as others who have an interest in exploring energy resource options and technologies with a view toward achieving sustainability on local, national, and global scales.
In Software Abstractions Daniel Jackson introduces an approach to software design that draws on traditional formal methods but exploits automated tools to find flaws as early as possible. This approach--which Jackson calls “lightweight formal methods” or “agile modeling”--takes from formal specification the idea of a precise and expressive notation based on a tiny core of simple and robust concepts but replaces conventional analysis based on theorem proving with a fully automated analysis that gives designers immediate feedback.