@inbook{benavides_baugh_gopalakrishnan_2023, title={An HPC Practitioner’s Workbench for Formal Refinement Checking}, url={https://doi.org/10.1007/978-3-031-31445-2_5}, DOI={10.1007/978-3-031-31445-2_5}, abstractNote={HPC practitioners make use of techniques, such as parallelism and sparse data structures, that are difficult to reason about and debug. Here we explore the role of data refinement, a correct-by-construction approach, in verifying HPC applications via bounded model checking. We show how single program, multiple data (SPMD) parallelism can be modeled in Alloy, a declarative specification language, and describe common issues that arise when performing scope-complete refinement checks in this context.}, booktitle={Languages and Compilers for Parallel Computing}, publisher={Springer Nature Switzerland}, author={Benavides, Juan and Baugh, John and Gopalakrishnan, Ganesh}, year={2023}, pages={64–72} }
 @article{zhang_teng_kong_baugh_su_mi_du_2023, title={Automatic modelling and verification of AUTOSAR architectures?}, volume={201}, ISSN={["1873-1228"]}, url={https://doi.org/10.1016/j.jss.2023.111675}, DOI={10.1016/j.jss.2023.111675}, abstractNote={Autosar (AUTomotive Open System ARchitecture) is a development partnership whose primary goal is the standardization of basic system functions and functional interfaces for electronic control units in automobiles. As an open specification, its layered software architecture promotes the interoperability of real-time embedded vehicle systems and components. It also opens up the possibility of formal modelling and verification approaches, centred around the specification, that can be used to support analysis in the early stages of design. In this paper, we describe a methodology and associated tool, called A2A, that automatically models systems defined by the Autosar specifications as timed automata, and then verifies their timing properties using Uppaal. It contains 22 groups of timed automata templates, together with two auxiliary test templates, that model the Autosar architecture and timing properties, allowing time-related behaviours to be extracted from the three-layer architecture, i.e., the Autosar Software, Autosar Runtime Environment, and Basic Software layers, and templates to be automatically instantiated. The timing properties are specified using timed computation tree logic (TCTL) in Uppaal to verify the system model. We demonstrate the capabilities of the methodology by applying it to an Autosar architecture that describes an internal vehicle light control system, thereby showing its effectiveness.}, journal={JOURNAL OF SYSTEMS AND SOFTWARE}, author={Zhang, Miaomiao and Teng, Yu and Kong, Hui and Baugh, John and Su, Yu and Mi, Junri and Du, Bowen}, year={2023}, month={Jul} }
 @inbook{banach_baugh_2023, title={Formalisation, Abstraction and Refinement of Bond Graphs}, url={https://doi.org/10.1007/978-3-031-36709-0_8}, DOI={10.1007/978-3-031-36709-0_8}, abstractNote={Bond graphs represent the structure and functionality of mechatronic systems from a power flow perspective. Unfortunately, presentations of bond graphs are replete with ambiguity, significantly impeding understanding. A formalisation of the essentials of bond graphs is given, together with a formalisation of bond graph transformation, which can directly express abstraction and refinement of bond graphs.}, author={Banach, Richard and Baugh, John}, year={2023} }
 @article{kwag_gupta_baugh_kim_2021, title={Significance of multi-hazard risk in design of buildings under earthquake and wind loads}, volume={243}, ISSN={["1873-7323"]}, DOI={10.1016/j.engstruct.2021.112623}, abstractNote={• Development of a performance-based framework to consider multiple hazards. • Significance of multi-hazard design is shown through retrofit solutions in buildings. • Cost-effective damper design is explored under two different hazards. Traditionally, external hazards are considered in the design of a building through the various combinations of loads prescribed in relevant design codes and standards. It is often the case that the design is governed by a single dominant hazard at a given geographic location. This is particularly true for earthquake and wind hazards, both of which impart time-dependent dynamic loads on the structure. Engineers may nevertheless wonder if a building designed for one of the two dominant hazards will satisfactorily withstand the other. Prior studies have indicated that in some cases, when a building is designed for a single dominant hazard, it does not necessarily provide satisfactory performance against the other hazard. In this paper, we propose a novel framework that builds upon performance-based design requirements and determines whether the design of a building is governed primarily by a single hazard or multiple hazards. It integrates site-dependent hazard characteristics with the performance criteria for a given building type and building geometry. The framework is consistent with the burgeoning area of probabilistic risk assessment, and yet can easily be extended to traditional, deterministically characterized design requirements as illustrated herein.}, journal={ENGINEERING STRUCTURES}, author={Kwag, Shinyoung and Gupta, Abhinav and Baugh, John and Kim, Hyun-Su}, year={2021}, month={Sep} }
 @inbook{banach_baugh_2020, place={Cham}, title={A simple Hybrid Event-B model of an active control system for
  earthquake protection}, volume={35}, DOI={10.1007/978-3-030-15792-0_7}, abstractNote={In earthquake-prone zones of the world, severe damage to buildings and life endangering harm to people pose a major risk when severe earthquakes happen. In recent decades, active and passive measures to prevent building damage have been designed and deployed. A simple model of an active damage prevention system, founded on earlier work, is investigated from a model based formal development perspective, using Hybrid Event-B. The non-trivial physical behaviour in the model is readily captured within the formalism. However, when the usual approximation and discretization techniques from engineering and applied mathematics are used, the rather brittle refinement techniques used in model based formal development start to break down. Despite this, the model developed stands up well when compared via simulation with a standard approach. The requirements of a richer formal development framework, better able to cope with applications exhibiting non-trivial physical elements are discussed.}, booktitle={From Astrophysics to Unconventional Computation}, publisher={Springer}, author={Banach, Richard and Baugh, John}, editor={Adamatzky, Andrew and Kendon, VivienEditors}, year={2020}, pages={157–194} }
 @inproceedings{dyer_altuntas_baugh_2019, title={Bounded Verification of Sparse Matrix Computations}, url={http://dx.doi.org/10.1109/correctness49594.2019.00010}, DOI={10.1109/correctness49594.2019.00010}, abstractNote={We show how to model and reason about the structure and behavior of sparse matrices, which are central to many applications in scientific computation. Our approach is state-based, relying on a formalism called Alloy to show that one model is a refinement of another. We present examples of sparse matrix-vector multiplication, transpose, and translation between formats using ELLPACK and compressed sparse row formats to demonstrate the approach. To model matrix computations in a declarative language like Alloy, a new idiom is presented for bounded iteration with incremental updates. Mechanical verification is performed using SAT solvers built into the tool.}, booktitle={2019 IEEE/ACM 3rd International Workshop on Software Correctness for HPC Applications (Correctness)}, publisher={IEEE/ACM}, author={Dyer, Tristan and Altuntas, Alper and Baugh, John}, year={2019}, month={Nov}, pages={36–43} }
 @article{baugh_altuntas_2018, title={Formal methods and finite element analysis of hurricane storm surge: A case study in software verification}, volume={158}, ISSN={["1872-7964"]}, url={https://doi.org/10.1016/j.scico.2017.08.012}, DOI={10.1016/j.scico.2017.08.012}, abstractNote={Used to predict the effects of hurricane storm surge, ocean circulation models are essential tools for evacuation planning, vulnerability assessment, and infrastructure design. Implemented as numerical solvers that operate on large-scale datasets, these models determine the geographic extent and severity of coastal floods and other impacts. In this study, we look at an ocean circulation model used in production and an extension made to it that offers substantial performance gains. To explore implementation choices and ensure soundness of the extension, we make use of Alloy, a declarative modeling language with tool support and an automatic form of analysis performed within a bounded scope using a SAT solver. Abstractions for relevant parts of the ocean circulation model are presented, including the physical representation of land and seafloor surfaces as a finite element mesh, and an algorithm operating on it that allows for the propagation of overland flows. The approach allows us to draw useful conclusions about implementation choices and guarantees about the extension, in particular that it is equivalence preserving. • An application of formal methods in the context of scientific computing and large-scale physical simulation. • Development of models in Alloy for analyzing relevant parts of an ocean circulation model used in production. • Guarantees about soundness of an extension supported by the approach through experimentation and analysis.}, journal={SCIENCE OF COMPUTER PROGRAMMING}, publisher={Elsevier BV}, author={Baugh, John and Altuntas, Alper}, year={2018}, month={Jun}, pages={100–121} }
 @article{altuntas_baugh_2018, title={Hybrid theorem proving as a lightweight method for verifying numerical software}, DOI={10.1109/Correctness.2018.00005}, abstractNote={Large-scale numerical software requires substantial computer resources that complicate testing and debugging. A single run of a climate model may require many millions of core-hours and terabytes of disk space, making trial-and-error experiments burdensome and time consuming. In this study, we apply hybrid theorem proving from the field of cyber-physical systems to problems in scientific computation, and show how to verify the correctness of discrete updates that appear in the simulation of continuous physical systems. By viewing numerical software as a hybrid system that combines discrete and continuous behavior, test coverage and confidence in findings can be increased. We describe abstraction approaches for modeling numerical software and demonstrate the applicability of the approach in a case study that reproduces undesirable behavior encountered in a parameterization scheme, called the K-profile parameterization, widely used in ocean components of large-scale climate models. We then identify and model a fix in the configuration of the scheme, and verify that the undesired behavior is eliminated for all possible execution sequences. We conclude that hybrid theorem proving is an effective and efficient approach that can be used to verify and reason about properties of large-scale numerical software.}, journal={PROCEEDINGS OF CORRECTNESS 2018: 2ND IEEE/ACM INTERNATIONAL WORKSHOP ON SOFTWARE CORRECTNESS FOR HPC APPLICATIONS}, publisher={IEEE}, author={Altuntas, Alper and Baugh, John}, year={2018}, pages={1–8} }
 @article{liu_jiang_yang_baugh_2018, title={Numerical study on factors influencing typhoon-induced storm surge distribution in Zhanjiang Harbor}, volume={215}, url={https://doi.org/10.1016/j.ecss.2018.09.019}, DOI={10.1016/j.ecss.2018.09.019}, abstractNote={A 2-D unstructured finite element model is used to study how local and remote atmospheric forcing, sea level rise, and shoreline variation affect typhoon-induced storm surge in a small shallow bay, Zhanjiang Harbor (ZH). In this research, the spatial distribution of storm surge is divided into three patterns in ZH, denoted E-W, N-S, and S-N, using a quantitative method. In the Bay, local atmospheric effects (LAE) and remote atmospheric effects (RAE) both play important roles in the maximum residual water level. The contribution of RAE to the inflow is higher than that of the LAE, but the former is less important in the spatial distribution in ZH. In addition, the typhoon track influences the time of occurrence of the maximum surge by forcing the outer waters to ZH, then the spatial distribution of the surge residual in the bay is controlled by local winds, and different regions are threatened during different kinds of storm surge processes. Two sea level rise scenarios are set up in the paper as well, and the results show that the trends of the changes in LAE and RAE in the inner-bay are the opposite in the case of sea level rise; however, the total changes of the distribution are not the same in different categories. In general, the E-W category storm surge is weakened, while the N-S and S-N category storm surges have inverse changes in the north and south of ZH. There is a downward trend of the maximum surge gradient within the Bay, but relative to sea level rise itself this effect is not obvious. The establishment of the sea embankment increased the storm surge within the bay though it is not significant.}, journal={Estuarine, Coastal and Shelf Science}, publisher={Elsevier BV}, author={Liu, Xing and Jiang, Wensheng and Yang, Bo and Baugh, John}, year={2018}, month={Dec}, pages={39–51} }
 @inproceedings{baugh_dyer_2018, place={Cham}, title={State-based formal methods in scientific computation}, DOI={10.1007/978-3-319-91271-4_29}, abstractNote={Control systems, protocols, and hardware design are among the most common applications of state-based formal methods, and yet the types of modeling and analysis they enable are also well-suited to problems in scientific computation, where quality, reproducibility, and productivity are growing concerns. We survey the challenges faced by developers of scientific software, characterize the nature of the programs they write, and offer some perspective on the role that state-based methods can play in scientific domains.}, note={Lecture Notes in Computer Science 10817}, booktitle={Abstract State Machines, Alloy, B, TLA, VDM, and Z}, publisher={Springer}, author={Baugh, John and Dyer, Tristan}, editor={Butler, Michael and Raschke, Alexander and Hoang, Thai Son and Reichl, KlausEditors}, year={2018}, pages={392–396} }
 @article{altuntas_baugh_2017, title={Adaptive subdomain modeling: A multi-analysis technique for ocean circulation models}, volume={115}, ISSN={["1463-5011"]}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-85020014888&partnerID=MN8TOARS}, DOI={10.1016/j.ocemod.2017.05.009}, abstractNote={Many coastal and ocean processes of interest operate over large temporal and geographical scales and require a substantial amount of computational resources, particularly when engineering design and failure scenarios are also considered. This study presents an adaptive multi-analysis technique that improves the efficiency of these computations when multiple alternatives are being simulated. The technique, called adaptive subdomain modeling, concurrently analyzes any number of child domains, with each instance corresponding to a unique design or failure scenario, in addition to a full-scale parent domain providing the boundary conditions for its children. To contain the altered hydrodynamics originating from the modifications, the spatial extent of each child domain is adaptively adjusted during runtime depending on the response of the model. The technique is incorporated in ADCIRC++, a re-implementation of the popular ADCIRC ocean circulation model with an updated software architecture designed to facilitate this adaptive behavior and to utilize concurrent executions of multiple domains. The results of our case studies confirm that the method substantially reduces computational effort while maintaining accuracy.}, journal={OCEAN MODELLING}, author={Altuntas, Alper and Baugh, John}, year={2017}, month={Jul}, pages={86–104} }
 @inproceedings{altuntas_baugh_2017, title={Verifying Concurrency in an Adaptive Ocean Circulation Model}, DOI={10.1145/3145344.3145346}, abstractNote={We present a model checking approach for verifying the correctness of concurrency in numerical models. The forms of concurrency we address are from (1) coupled modeling where distinct components, e.g., ocean, wave, and atmospheric, exchange interface conditions during runtime, and (2) multi-instance modeling where local variations of the same numerical model are executed concurrently to minimize common (and therefore redundant) computations. We present general guidelines for representing these forms of concurrency in an abstract verification model and then apply them to an adaptive ocean circulation model that determines the geographic extent and severity of coastal floods. The ocean model employs multi-instance concurrency: a collection of engineering design and failure scenarios are concurrently simulated using patches, regions of a grid that grow and shrink based on the hydrodynamic changes induced by each scenario. We show how concurrency inherent in the simulation model can be represented in a verification model to ensure correctness and to automatically generate safe synchronization arrangements.}, booktitle={Proceedings of the First International Workshop on Software Correctness for HPC Applications  - Correctness'17}, publisher={ACM Press}, author={Altuntas, Alper and Baugh, John}, year={2017} }
 @article{baugh_liu_2016, title={A general characterization of the Hardy Cross method as sequential and multiprocess algorithms}, volume={6}, ISSN={["2352-0124"]}, DOI={10.1016/j.istruc.2016.03.004}, abstractNote={The Hardy Cross method of moment distribution admits, for any problem, an entire family of distribution sequences. Intuitively, the method involves clamping the joints of beams and frames against rotation and balancing moments iteratively, whether consecutively, simultaneously, or in some combination of the two. We present common versions of the moment distribution algorithm and generalizations of them as both sequential and multiprocess algorithms, with the latter exhibiting the full range of asynchronous behavior allowed by the method. We prove, in the limit, that processes so defined converge to the same unique solution regardless of the distribution sequence or interleaving of steps. In defining the algorithms, we avoid overspecifying the order of computation initially using a sequential, nondeterministic process, and then more generally using concurrent processes.}, journal={STRUCTURES}, publisher={Elsevier BV}, author={Baugh, John and Liu, Shu}, year={2016}, month={May}, pages={170–181} }
 @article{baugh_altuntas_2016, place={Cham}, title={Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy}, volume={9675}, ISBN={["978-3-319-33599-5"]}, ISSN={["1611-3349"]}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-84978698635&partnerID=MN8TOARS}, DOI={10.1007/978-3-319-33600-8_18}, abstractNote={We describe an Alloy model that helps check the correctness of a discrete wet-dry algorithm used in a system for hurricane storm surge prediction. Derived from simplified physics and encoded with empirical rules, the algorithm operates on a finite element mesh to allow the propagation of overland flows. Our study is motivated by complex interactions between the algorithm and a recent performance enhancement to the system that involves mesh partitioning. We briefly outline our approach and describe safety properties of the extension, as well as directions for future work.}, note={Lecture Notes in Computer Science 9675}, journal={ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016)}, publisher={Springer}, author={Baugh, John and Altuntas, Alper}, editor={Butler, Michael and Schewe, Klaus-Dieter and Mashkoor, Atif and Biro, MiklosEditors}, year={2016}, pages={256–261} }
 @article{dyer_baugh_2016, title={SMT: An interface for localized storm surge modeling}, volume={92}, ISSN={["1873-5339"]}, DOI={10.1016/j.advengsoft.2015.10.003}, abstractNote={The devastation wrought by Hurricanes Katrina (2005), Ike (2008), and Sandy (2012) in recent years continues to underscore the need for better prediction and preparation in the face of storm surge and rising sea levels. Simulations of coastal flooding using physically based hydrodynamic codes like ADCIRC, while very accurate, are also computationally expensive, making them impractical for iterative design scenarios that seek to evaluate a range of countermeasures and possible failure points. We present a graphical user interface that supports local analysis of engineering design alternatives based on an exact reanalysis technique called subdomain modeling, an approach that substantially reduces the computational effort required. This interface, called the Subdomain Modeling Tool (SMT), streamlines the pre- and post-processing requirements of subdomain modeling by allowing modelers to extract regions of interest interactively and by organizing project data on the file system. Software design and implementation issues that make the approach practical, such as a novel range search algorithm, are presented. Descriptions of the overall methodology, software architecture, and performance results are given, along with a case study demonstrating its use.}, journal={ADVANCES IN ENGINEERING SOFTWARE}, publisher={Elsevier BV}, author={Dyer, Tristan and Baugh, John}, year={2016}, month={Feb}, pages={27–39} }
 @article{baugh_altuntas_dyer_simon_2015, title={An exact reanalysis technique for storm surge and tides in a geographic region of interest}, volume={97}, ISSN={["1872-7379"]}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-85027939365&partnerID=MN8TOARS}, DOI={10.1016/j.coastaleng.2014.12.003}, abstractNote={Understanding the effects of storm surge in hurricane-prone regions is necessary for protecting public and lifeline services and improving resilience. While coastal ocean hydrodynamic models like ADCIRC may be used to assess the extent of inundation, the computational cost may be prohibitive since many local changes corresponding to design and failure scenarios would ideally be considered. We present an exact reanalysis technique and corresponding implementation that enable the assessment of local subdomain changes with less computational effort than would be required by a complete resimulation of the full domain. So long as the subdomain is large enough to fully contain the altered hydrodynamics, changes may be made and simulations performed within it without the need to calculate new boundary values. Accurate results are obtained even when subdomain boundary conditions are forced only intermittently, and convergence is demonstrated by progressively increasing the frequency at which they are applied. Descriptions of the overall methodology, performance results, and accuracy, as well as case studies, are presented.}, journal={COASTAL ENGINEERING}, author={Baugh, John and Altuntas, Alper and Dyer, Tristan and Simon, Jason}, year={2015}, month={Mar}, pages={60–77} }
 @article{the effects of construction related costs on the optimization of steel frames_2012, volume={43}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-84863199832&partnerID=MN8TOARS}, DOI={10.12989/sem.2012.43.1.031}, abstractNote={This paper presents a computational study that explores the design of rigid steel frames by considering construction related costs. More specifically, two different aspects are investigated in this study focusing on the effects of (a) reducing the number of labor intensive rigid connections within a frame of given geometric layout, and (b) reducing the number of different member section types used in 
the frame. A genetic algorithm based optimization framework searches design space for these objectives. Unlike some studies that express connection cost as a factor of the entire frame weight, here connections and their associated cost factors are explicitly represented at the member level to evaluate the cost of connections associated with each beam. In addition, because variety in member section types can drive up construction related costs, its effects are evaluated implicitly by generating curves that show the trade off between cost and different numbers of section types used within the frame. Our results show that designs 
in which all connections are considered to be rigid can be excessively conservative: rigid connections can often be eliminated without any appreciable increase in frame weight, resulting in a reduction in overall cost. Eliminating additional rigid connections leads to further reductions in cost, even as frame weight increases, up to a certain point. These complex relationships between overall cost, rigid connections, and member section types are presented for a representative five-story steel frame.}, number={1}, journal={Structural Engineering and Mechanics}, year={2012}, pages={31–51} }
 @article{kripakaran_gupta_baugh_2007, title={A novel optimization approach for minimum cost design of trusses}, volume={85}, ISSN={["1879-2243"]}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-36049020582&partnerID=MN8TOARS}, DOI={10.1016/j.compstruc.2007.04.006}, abstractNote={This paper describes new optimization strategies that offer significant improvements in performance over existing methods for bridge-truss design. In this study, a real-world cost function that consists of costs on the weight of the truss and the number of products in the design is considered. We propose a new sizing approach that involves two algorithms applied in sequence – (1) a novel approach to generate a “good” initial solution and (2) a local search that attempts to generate the optimal solution by starting with the final solution from the previous algorithm. A clustering technique, which identifies members that are likely to have the same product type, is used with cost functions that consider a cost on the number of products. The proposed approach gives solutions that are much lower in cost compared to those generated in a comprehensive study of the same problem using genetic algorithms (GA). Also, the number of evaluations needed to arrive at the optimal solution is an order of magnitude lower than that needed in GAs. Since existing optimization techniques use cost functions like those of minimum-weight truss problems to illustrate their performance, the proposed approach is also applied to the same examples in order to compare its relative performance. The proposed approach is shown to generate solutions of not only better quality but also much more efficiently. To highlight the use of this sizing approach in a broader optimization framework, a simple geometry optimization algorithm that uses the sizing approach is presented. This algorithm is also shown to provide solutions better than the existing results in literature.}, number={23-24}, journal={COMPUTERS & STRUCTURES}, author={Kripakaran, Prakash and Gupta, Abhinav and Baugh, John W., Jr.}, year={2007}, month={Dec}, pages={1782–1794} }
 @article{kumar_doby_baugh_brill_ranjithan_2007, title={Closure to "optimal design of redundant water distribution networks using a cluster of workstations" by Sujay V. Kumar, Troy A. Doby, John W. Baugh Jr., E. Downey Brill, and S. Ranji Ranjithan}, volume={133}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-36349011269&partnerID=MN8TOARS}, DOI={10.1061/(asce)0733-9496(2007)133:6(580)}, number={6}, journal={Journal of Water Resources Planning and Management}, author={Kumar, S. V. and Doby, T. A. and Baugh, John and Brill, E. D. and Ranjithan, S. R.}, year={2007}, pages={580–581} }
 @article{kumar_doby_baugh_brill_ranjithan_2006, title={Optimal design of redundant water distribution networks using a cluster of workstations}, volume={132}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-33747304468&partnerID=MN8TOARS}, DOI={10.1061/(ASCE)0733-9496(2006)132:5(374)}, abstractNote={A genetic algorithm (GA)-based method for the least-cost design of looped pipe networks for various levels of redundancy is presented in this paper. Redundancy constraints are introduced in the optimization model by considering the number of pipes assumed to be out of service at any one time. Using this approach, trade-off relationships between cost and redundancy are developed. The GA-based approach is computationally intensive, and implementations on a custom fault-tolerant distributed computing framework, called Vitri, are used to satisfy the computational requirements. The design methodology is applied to two water distribution networks of different sizes, and a comparison of the performance of the distributed GAs for the design problems is also presented. We conclude that a GA-based approach to obtaining cost-effective, redundant solutions for the least-cost design of looped pipe networks can be effectively used on a heterogeneous network of nondedicated workstations.}, number={5}, journal={Journal of Water Resources Planning and Management}, author={Kumar, S. V. and Doby, T. A. and Baugh, John and Brill, E. D. and Ranjithan, S. R.}, year={2006}, pages={374–384} }
 @article{gupta_kripakaran_mahinthakumar_baugh_2005, title={Genetic algorithm-based decision support for optimizing seismic response of piping systems}, volume={131}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-14544294041&partnerID=MN8TOARS}, DOI={10.1061/(asce)0733-9445(2005)131:3(389)}, abstractNote={This paper describes computational approaches used in a prototype decision support system (DSS) for seismic design and performance evaluation of piping supports. The DSS is primarily based on a genetic algorithm (GA) that uses finite element analyses, and an existing framework for high performance distributed computing on workstation clusters. A detailed discussion is presented on various issues related to the development of an efficient GA implementation for evaluating the trade-off between the number of supports and cost. An integer string representation of the type used in some existing studies, for instance, is shown to be inferior to a binary string representation, which is appropriate when supports are modeled as axially rigid. A novel seeding technique, which overcomes the inefficiencies of conventional methods in the context of pipe support optimization, is also presented. Finally, an efficient crossover scheme is proposed for generating trade-off curves and the approach is validated with respect ...}, number={3}, journal={Journal of Structural Engineering}, author={Gupta, A. and Kripakaran, P. and Mahinthakumar, G. K. and Baugh, J. W.}, year={2005}, pages={389–398} }
 @inproceedings{doby_kumar_baugh_brill_ranjithan_2004, title={Genetic algorithm search for least cost design of looped pipe networks using age as a quality surrogate and different levels of redundancy}, volume={111}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-75649129137&partnerID=MN8TOARS}, DOI={10.1061/40569(2001)387}, abstractNote={A genetic algorithm- (GA-) based method is being investigated for determining the least cost design of looped networks while considering the residence time of the water in the network as a quality surrogate and various levels of redundancy. The conflict among the three design objectives, i.e., cost, redundancy, and water quality, is examined via multiobjective analysis.}, booktitle={Bridging the Gap: Meeting the World's Water and Environmental Resources Challenges - Proceedings of the World Water and Environmental Resources Congress 2001}, author={Doby, T.A. and Kumar, S.V. and Baugh, J.W. and Brill, E.D. and Ranjithan, S.R.}, year={2004} }
 @inproceedings{kumar_doby_baugh_brill_ranjithan_2004, title={Method for least cost design of looped pipe networks for different levels of redundancy using genetic algorithms}, volume={104}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-74949091879&partnerID=MN8TOARS}, DOI={10.1061/40517(2000)201}, abstractNote={A new method is proposed for the least cost design of looped piped networks under various levels of redundancy using a genetic algorithm. Various levels of redundancy can be obtained by considering the number of pipes to be taken out of service at any one time. As a result, a tradeoff curve of redundancy and cost can be developed. The approach is being extended to consider different measures of redundancy as well as other performance criteria. Such extensions are more computationally demanding and are therefore being implemented using a distributed GA.}, booktitle={Joint Conference on Water Resource Engineering and Water Resources Planning and Management 2000: Building Partnerships}, author={Kumar, S.V. and Doby, T.A. and Baugh, J.W. and Brill, E.D. and Ranjithan, S.R.}, year={2004} }
 @inproceedings{vitri: a framework for environmental decision support on heterogeneous computer networks_2004, volume={111}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-75649149870&partnerID=MN8TOARS}, DOI={10.1061/40569(2001)111}, abstractNote={Vitri is an object-oriented framework implemented in Java for high-performance distributed computing. Using Vitri, applications can engage in cooperative problem solving by dividing their tasks among heterogeneous clusters of workstations and PCs. Vitri's features include basic support for distributed computing and communication, as well as visual tools for evaluating run-time performance, and modules for heuristic optimization. It balances loads dynamically using a client-side task pool, allows the addition or removal of servers dating a run, and provides fault tolerance transparently for servers and networks. Among its more powerful features are modules for heuristic optimization, including an asynchronous global-parallel genetic algorithm that is particularly suited for coarse-grained tasks executing on processors with large variations in processor speeds. By using dataflow techniques, in which computations are explicitly based on the availability and forwarding of data, the usual end-of-generation synchronization points are removed from the algorithm. Results are presented for illustrative applications in water distribution network design and air quality management.}, booktitle={Bridging the Gap: Meeting the World's Water and Environmental Resources Challenges - Proceedings of the World Water and Environmental Resources Congress 2001}, year={2004} }
 @book{asynchronous genetic algorithms for heterogeneous networks using coarse-grained dataflow_2003, volume={2723}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-35248893482&partnerID=MN8TOARS}, journal={Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}, year={2003}, pages={730–741} }
 @inbook{baugh_kumar_2003, title={Asynchronous genetic algorithms for heterogenous networks using course-grained dataflow}, volume={2723}, ISBN={3540406026}, DOI={10.1007/3-540-45105-6_88}, abstractNote={Genetic algorithms (GAs) are an attractive class of techniques for solving a variety of complex search and optimization problems. Their implementation on a distributed platform can provide the necessary computing power to address large-scale problems of practical importance. On heterogeneous networks, however, the performance of a global parallel GA can be limited by synchronization points during the computation, particularly those between generations. We present a new approach for implementing asynchronous GAs based on the dataflow model of computation — an approach that retains the functional properties of a global parallel GA. Experiments conducted with an air quality optimization problem and others show that the performance of GAs can be substantially improved through dataflow-based asynchrony.}, booktitle={Genetic and evolutionary computation--GECCO 2003: Genetic and Evolutionary Computation Conference, Chicago, IL, USA, July 12-16, 2003: Proceedings}, publisher={Berlin; New York: Springer}, author={Baugh, J. W. and Kumar, S. V.}, year={2003}, pages={730–741} }
 @inproceedings{new ga approaches for pipe support optimization_2003, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-22344433506&partnerID=MN8TOARS}, booktitle={Proceedings of the Structures Congress and Exposition}, year={2003}, pages={61–62} }
 @article{baugh_konduri_2001, title={Discrete element modelling on a cluster of workstations}, volume={17}, ISSN={["0177-0667"]}, DOI={10.1007/PL00007192}, number={1}, journal={ENGINEERING WITH COMPUTERS}, author={Baugh, JW and Konduri, RKS}, year={2001}, pages={1–15} }
 @article{j.w._konduri_2001, title={Discrete element modelling on a cluster of workstations}, volume={17}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0035194161&partnerID=MN8TOARS}, number={1}, journal={Engineering with Computers}, author={J.W., Baugh, Jr. and Konduri, R.K.S.}, year={2001}, pages={1–15} }
 @article{loughlin_ranjithan_brill_baugh_2001, title={Genetic algorithm approaches for addressing unmodeled objectives in optimization problems}, volume={33}, ISSN={["0305-215X"]}, DOI={10.1080/03052150108940933}, abstractNote={Abstract Public sector decision-making typically involves complex problems that are often not completely understood. In these problems, there are invariably unmodeled issues that can greatly impact the acceptability of solutions. Modeling to Generate Alternatives (MGA) is an approach for addressing unmodeled issues in an optimization context. MGA techniques are used to generate a small number of good, yet very different, solutions to optimization problems. Because these solutions are different in decision space, they may differ considerably in performance when unmodeled objectives are considered. Many problems are sufficiently complex that traditional optimization solution procedures, and therefore traditional MGA techniques, are not readily applicable. Two techniques for performing MGA using genetic algorithms (GAs) are investigated and compared. One of these techniques, which uses specialized MGA operators, is shown to produce solutions that are both better in quality and more different. This technique is also demonstrated for a realistic air quality management problem.}, number={5}, journal={ENGINEERING OPTIMIZATION}, author={Loughlin, DH and Ranjithan, SR and Brill, ED and Baugh, JW}, year={2001}, pages={549–569} }
 @article{genetic algorithm approaches for addressing unmodeled objectives in optimization problems_2001, volume={33}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-2342512900&partnerID=MN8TOARS}, number={5}, journal={Engineering Optimization}, year={2001}, pages={549–569} }
 @book{stone_baugh_chakravarty_surasky_2001, title={Winston-Salem Mobility Manager: Data collection, validation, and performance evaluation}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0035728022&partnerID=MN8TOARS}, number={1760}, journal={Transportation Research Record}, author={Stone, J.R. and Baugh, J.W. and Chakravarty, S. and Surasky, M.N.}, year={2001}, pages={114–120} }
 @inbook{stone_baugh_chakravarty_surasky_2001, title={Winston-Salem mobility manager: Data collection, validation, and performance evaluation}, ISBN={0309072220}, DOI={10.3141/1760-15}, abstractNote={ The Winston-Salem Mobility Manager project has served as a test bed for advanced public transportation systems technology since 1995. The aspects of remote data collection, validation, and performance evaluation are discussed. The computerized scheduling software for Trans-AID, the local paratransit system, was accessed and passenger RIDE files were downloaded. Java-based utilities and conventional spreadsheets removed invalid data, sorted urban and rural passenger trips, and compared transit productivity measures. Validated Trans-AID data show relatively few data entry errors, some logical errors, and high time-window violations. Ridership, productivity, and service gains determined by intuitive assessment of traditional measures are not supported by statistical analysis. Rather, the results of t-tests suggest counterintuitive management actions to improve service and productivity. Internet-based methods of data collection, validation, and evaluation demonstrate promise for real-time transit management and agency monitoring. }, number={1760}, booktitle={Transit: Bus transit and maintenance: Rural paratransit technology: Capacity and quality of service}, publisher={Washington, DC: National Academy Press}, author={Stone, J. R. and Baugh, J. W. and Chakravarty, S. and Surasky, M. N.}, year={2001}, pages={114–120} }
 @article{loughlin_ranjithan_baugh_brill_2000, title={Application of genetic algorithms for the design of ozone control strategies}, volume={50}, ISSN={["2162-2906"]}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0034195231&partnerID=MN8TOARS}, DOI={10.1080/10473289.2000.10464133}, abstractNote={ABSTRACT Designing air quality management strategies is complicated by the difficulty in simultaneously considering large amounts of relevant data, sophisticated air quality models, competing design objectives, and unquantifiable issues. For many problems, mathematical optimization can be used to simplify the design process by identifying cost-effective solutions. Optimization applications for controlling nonlinearly reactive pollutants such as tropospheric ozone, however, have been lacking because of the difficulty in representing nonlinear chemistry in mathematical programming models. We discuss the use of genetic algorithms (GAs) as an alternative optimization approach for developing ozone control strategies. A GA formulation is described and demonstrated for an urban-scale ozone control problem in which controls are considered for thousands of pollutant sources simultaneously. A simple air quality model is integrated into the GA to represent ozone transport and chemistry. Variations of the GA formulation for multiobjective and chance-constrained optimization are also presented. The paper concludes with a discussion of the practicality of using more sophisticated, regulatory-scale air quality models with the GA. We anticipate that such an approach will be practical in the near term for supporting regulatory decision-making.}, number={6}, journal={JOURNAL OF THE AIR & WASTE MANAGEMENT ASSOCIATION}, author={Loughlin, DH and Ranjithan, SR and Baugh, JW and Brill, ED}, year={2000}, month={Jun}, pages={1050–1063} }
 @article{baugh_kakivaya_2000, title={Finite state verification of intelligent transportation systems}, volume={14}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0033723981&partnerID=MN8TOARS}, DOI={10.1061/(ASCE)0887-3801(2000)14:1(38)}, abstractNote={Intelligent transportation systems (ITS) represent a major initiative to improve roadway and travel conditions, not by building roads, but by drawing on new technologies in computing, sensing, and communications. However, these technologies are extremely complex and, while some demonstration projects have tested stand-alone systems, the broader architectural and standardization issues are still under development. The use of complex technologies in a safety-critical system such as ITS and at the scale envisioned requires a very careful study of the interaction between its various subsystems. This paper describes an approach for modeling the temporal aspects of ITS systems as well as their logical coordination using finite state verification tools. The approach is demonstrated by verifying safety properties of an automated traffic signal at a road intersection.}, number={1}, journal={Journal of Computing in Civil Engineering}, author={Baugh, J. W. and Kakivaya, G. R.}, year={2000}, pages={38–50} }
 @article{chadha_baugh_wing_1999, title={Formal specification of concurrent systems}, volume={30}, ISSN={["0965-9978"]}, DOI={10.1016/S0965-9978(98)00058-1}, abstractNote={This paper presents a formal methodology for developing concurrent systems. We extend the Larch family of specification languages and tools with the CCS process algebra to support the specification and verification of concurrent systems. We present and follow a refinement strategy that relates an implementation in a programming language to a formal specification of such a system. We illustrate our methodology on an example that uses the preconditioned conjugate gradient method for solving a linear system of equations.}, number={3}, journal={ADVANCES IN ENGINEERING SOFTWARE}, author={Chadha, HS and Baugh, JW and Wing, JM}, year={1999}, month={Mar}, pages={211–224} }
 @article{formal specification of concurrent systems_1999, volume={30}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0033098338&partnerID=MN8TOARS}, number={3}, journal={Advances in Engineering Software}, year={1999}, pages={211–224} }
 @inproceedings{baugh_1998, title={A Web-based computing environment for structural analysis and design}, volume={1}, booktitle={Structural engineering world wide 1998: Proceedings of the Structural Engineers World Congress, July 19-23, 1998, San Francisco, California}, author={Baugh, J. W., Jr.}, year={1998}, pages={T140–1} }
 @inbook{baugh_1998, title={Design and verification of real-time systems}, volume={1454}, ISBN={3540648062}, DOI={10.1007/bfb0030441}, abstractNote={Advances in sensing, effecting, and computational technologies will change the way we design, construct, and monitor systems that interact with the physical world. Building structures will sense and respond to external loads, autonomous robots will occupy construction sites, and intelligent vehicles will monitor network flows to circumvent delays. As engineers, we must be prepared to work with the information technologies that underpin these coming systems. This paper addresses several of the prominent technical concerns in designing real-time systems that control some aspect of their environment. The view taken is that, by considering software systems to be an engineering artifact, we can begin to develop the kinds of quantitative approaches found in other areas of engineering design.}, booktitle={Artificial intelligence in structural engineering: Information technology for design, collaboration, maintenance, and monitoring}, publisher={Berlin; New York: Springer}, author={Baugh, J. W.}, year={1998}, pages={30–47} }
 @article{baugh_kakivaya_stone_1998, title={Intractability of the dial-a-ride problem and a multiobjective solution using simulated annealing}, volume={30}, ISSN={["0305-215X"]}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0031680443&partnerID=MN8TOARS}, DOI={10.1080/03052159808941240}, abstractNote={Abstract Numerous techniques for generating approximate solutions have been proposed in the last decade for routing and scheduling in multi-vehicle dial-a-ride problems. While some of these techniques have mathematical foundations, it is often difficult to assess the global optimality of the generated solution due to the use of pure local improvement methods. In additon, most of these methods are based on a single objective, such as minimization of the number of vehicles used, and cannot account for different or competing objectives that characterize the problem. This paper proves the intractability of the dial-a-ride problem, and then describes a new approximate method based on simulated annealing that is used to solve these problems in the presence of multiple objectives.}, number={2}, journal={ENGINEERING OPTIMIZATION}, author={Baugh, JW and Kakivaya, GKR and Stone, JR}, year={1998}, pages={91–123} }
 @inproceedings{loughlin_ranjithan_brill_baugh_fine_1998, title={Prototype decision support tool for developing tropospheric ozone control strategies}, booktitle={Water resources and the urban environment-98: Proceedings of the 1998 National Conference on Environmental Engineering. ASCE Joint 25th Annual Conference on Water Resources Planning and Management and 1998 National Conference on Environmental Engineering, Chicago, IL, June 7-10,1998}, publisher={Reston, VA: American Society of Civil Engineers}, author={Loughlin, D. and Ranjithan, S. and Brill, E. D. and Baugh, J. and Fine, S.}, year={1998} }
 @article{baugh_caldwell_brill_1997, title={A mathematical programming approach for generating alternatives in discrete structural optimization}, volume={28}, ISSN={["0305-215X"]}, DOI={10.1080/03052159708941125}, abstractNote={Structural design, like other complex decision problems, involves many tradeoffs among competing criteria. While mathematical programming models are increasingly realistic, there are often relevant issues that cannot be easily captured, if at all, in a formal system. This paper describes an approach to modelling that recognizes these limitations and allows a designer to explore unmodelled issues in a joint human-computer cognitive system. A prototype based on this approach is presented for topological truss optimization, and three modelling techniques are contrasted for their effectiveness in producing “different” alternatives. The results show that alternatives produced using these techniques are good with respect to modelled objectives, and yet are different, and often better, with respect to interesting objectives not present in the model.}, number={1-2}, journal={ENGINEERING OPTIMIZATION}, author={Baugh, JW and Caldwell, SC and Brill, ED}, year={1997}, pages={1–31} }
 @article{a mathematical programming approach for generating alternatives in discrete structural optimization_1997, volume={28}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0030703305&partnerID=MN8TOARS}, number={1-2}, journal={Engineering Optimization}, year={1997}, pages={1–31} }
 @article{elseaidy_cleaveland_baugh_1997, title={Modeling and verifying active structural control systems}, volume={29}, ISSN={["1872-7964"]}, DOI={10.1016/S0167-6423(96)00031-7}, abstractNote={This paper presents the results of a case study involving the use of a formal graphical notation, Modechart, and an automatic verification tool, the Concurrency Workbench, in the analysis of the design of a fault-tolerant active structural control system. Such control systems must satisfy strict requirements on their timing behavior; we show how to use various equivalence-based features supported by the Workbench to examine the timing behavior of different design alternatives, one of which has in excess of 1019 states. The central insight arising from the study involves the importance of compositionality for reasoning about large and complex systems; in particular, the success of the case study depends integrally on our notation's and tool's support of componentwise minimization.}, number={1-2}, journal={SCIENCE OF COMPUTER PROGRAMMING}, author={Elseaidy, WM and Cleaveland, R and Baugh, JW}, year={1997}, month={Jul}, pages={99–122} }
 @article{modeling and verifying active structural control systems_1997, volume={29}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0031185496&partnerID=MN8TOARS}, number={1-2}, journal={Science of Computer Programming}, year={1997}, pages={99–122} }
 @article{baugh_chadha_1997, title={Semantic validation of product and process models}, volume={11}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0343536396&partnerID=MN8TOARS}, DOI={10.1061/(ASCE)0887-3801(1997)11:1(26)}, abstractNote={This paper describes the use of equational specifications and process algebras in developing product and process models. These formal approaches enable an abstract and precise description of products, where both syntactic and semantic checks are used for validation. In addition, refinement methodologies are provided that relate the abstract specifications to implementations in data modeling languages such as EXPRESS. We show how these formal approaches, initially designed for specifying software and hardware modules, relate to current standards and research in product and process modeling. Our approach is illustrated with examples of both product and process modeling. The general architecture engineering and construction reference model (GARM) is modeled in an equational style using the Larch family of specification languages. The partitioned engineering data flow model (PANDA), a graphical approach for describing process models in facility engineering, is modeled as a process algebraic system in calculus of communicating systems (CCS). Both examples are validated by proving that they satisfy certain syntactic and semantic properties.}, number={1}, journal={Journal of Computing in Civil Engineering}, author={Baugh, J. W. and Chadha, H. S.}, year={1997}, pages={26–36} }
 @inproceedings{a controlled comparison of traditional classroom instruction with computer based instruction in an engineering class_1996, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-8744254801&partnerID=MN8TOARS}, booktitle={ASEE Annual Conference Proceedings}, year={1996}, pages={31–35} }
 @inproceedings{formal specification of concurrent finite element systems_1996, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0029735025&partnerID=MN8TOARS}, booktitle={Proceedings of the Conference on Analysis and Computation}, year={1996}, pages={166–176} }
 @article{network-distributed finite element analysis_1996, volume={25}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0030102588&partnerID=MN8TOARS}, number={2-3}, journal={Advances in Engineering Software}, year={1996}, pages={267–280} }
 @article{verification of an active control system using temporal process algebra_1996, volume={12}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0029753271&partnerID=MN8TOARS}, number={1}, journal={Engineering with Computers}, year={1996}, pages={46–61} }
 @inproceedings{verifying the timing requirements of multiprocessor control systems_1996, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0029736047&partnerID=MN8TOARS}, booktitle={Proceedings of the Conference on Analysis and Computation}, year={1996}, pages={278–285} }
 @inproceedings{loughlin_neal_ranjithan_brill_baugh_1995, title={Decision support system for air quality management}, volume={2}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0029238746&partnerID=MN8TOARS}, booktitle={Computing in Civil Engineering (New York)}, author={Loughlin, Daniel H. and Neal, J.Kevin and Ranjithan, S. and Brill, E.Downey and Baugh, John W.}, year={1995}, pages={1367–1374} }
 @inproceedings{multiobjective optimization of the dial-a-ride problem using simulated annealing_1995, volume={1}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0029229542&partnerID=MN8TOARS}, booktitle={Computing in Civil Engineering (New York)}, year={1995}, pages={278–285} }
 @article{baugh_elseaidy_1995, title={Real-time software development with formal models}, volume={9}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0028977227&partnerID=MN8TOARS}, DOI={10.1061/(ASCE)0887-3801(1995)9:1(73)}, abstractNote={Improvements in microprocessor technology have prompted a willingness to embed computer hardware in structural and mechanical systems. Active structural control is one such application in which computer-based sensors and actuators work to limit vibrations and reduce the possibility of failure in seismic events. Although there have been numerous studies on control strategies for these real-time systems, our goal is to develop approaches that can ensure the overall reliability of the software before deployment. In this paper, we outline a three-step approach based on formal methods for designing reliable real-time systems. This approach includes an analysis of the required timing properties, a modeling technique based on real-time logic and Modechart, and a verification procedure using simulation and model checking. As demonstrated with an application to structural control, this process ensures that the necessary timing properties are satisfied by a given hardware and software architecture.}, number={1}, journal={Journal of Computing in Civil Engineering}, author={Baugh, J.W. and Elseaidy, W.M.}, year={1995}, pages={73–86} }
 @article{evaluation of distributed finite element algorithms on a workstation network_1994, volume={10}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0028257276&partnerID=MN8TOARS}, DOI={10.1007/BF01206539}, number={1}, journal={Engineering with Computers}, year={1994}, pages={45–62} }
 @inproceedings{formal specification of aec product models_1994, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0028561189&partnerID=MN8TOARS}, number={1}, booktitle={Computing in Civil Engineering (New York)}, year={1994}, pages={571–578} }
 @inproceedings{modeling to generate alternatives in discrete structural optimization_1994, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0028580898&partnerID=MN8TOARS}, number={1}, booktitle={Computing in Civil Engineering (New York)}, year={1994}, pages={310–317} }
 @inproceedings{timing analysis of a multiprocessor architecture for active control_1994, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0028324006&partnerID=MN8TOARS}, booktitle={Analysis and Computation}, year={1994}, pages={203–212} }
 @inproceedings{verifying an intelligent structural control system: a case study_1994, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-84882667548&partnerID=MN8TOARS}, DOI={10.1109/REAL.1994.342708}, abstractNote={Describes the formal verification of the timing properties of the design of an intelligent structural control system using the Concurrency Workbench, an automatic verification tool for finite-state processes. The high-level design of the system is first given in Modechart, a graphical specification language for real-time systems, and then translated into a temporal process algebra supported by the Workbench. The facilities provided by this tool are then used to analyze the system and ultimately show it to be correct.<<ETX>>}, booktitle={Proceedings - Real-Time Systems Symposium}, year={1994}, pages={271–275} }
 @article{a client-server approach for distributed finite element analysis_1993, volume={17}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0027839250&partnerID=MN8TOARS}, DOI={10.1016/0965-9978(93)90043-S}, abstractNote={The prevalence of local area networks has made the combined processing power of interconnected workstations a compelling alternative to mainframe computers for computer-intensive analyses. We describe a methodology for developing finite element algorithms that distributes workload over an arbitrary number of network-connected computers. The approach employs a client-server model in which conventional Unix processes execute concurrently on a number of workstations and exchange information by sending messages over an Ethernet. The simplicity and flexibility of the model sets it apart from other approaches for distributed programming. Our approach shows impressive overall speedup for finite element analysis, even for small problem sizes.}, number={2}, journal={Advances in Engineering Software}, year={1993}, pages={69–78} }
 @inproceedings{creating interactive animated instructional programs on a unix-based workstation_1993, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-8744311160&partnerID=MN8TOARS}, DOI={10.1109/FIE.1993.405565}, abstractNote={The authors describe the development of a series of interactive, animated instructional programs for DEC stations at North Carolina University. The goal of the project is to develop three instructional units and test them in a controlled experiment in an undergraduate engineering course versus traditional instruction. The project team selected the cT program as the computing package to program the units. The three instructional units were developed for an undergraduate course in traffic engineering. Each unit deals with a different type of problem. The design unit concentrates on vertical highway alignment design and is very open-ended. The analysis unit guides the student through trip generation and is relatively closed-ended. The background unit presents the basic principles of surveying and should serve as a review of prerequisite material for most students.<<ETX>>}, booktitle={Proceedings - Frontiers in Education Conference, FIE}, year={1993}, pages={70–75} }
 @inproceedings{optimal resource leveling using integer-linear programming_1993, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0027306405&partnerID=MN8TOARS}, booktitle={Computing in Civil and Building Engineering}, year={1993}, pages={501–508} }
 @inproceedings{baugh_elseaidy_1993, title={Verification of real-time software for active structural control}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0027188290&partnerID=MN8TOARS}, booktitle={Computing in Civil and Building Engineering}, author={Baugh, John W. and Elseaidy, Wael M.}, year={1993}, pages={1672–1679} }
 @article{applications of coarse-grained dataflow in computational mechanics_1992, volume={8}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-33747303296&partnerID=MN8TOARS}, DOI={10.1007/BF01206334}, number={1}, journal={Engineering with Computers}, year={1992}, pages={13–30} }
 @article{baugh_rehak_1992, title={Data abstraction in engineering software development}, volume={6}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0026899312&partnerID=MN8TOARS}, DOI={10.1061/(ASCE)0887-3801(1992)6:3(282)}, abstractNote={Large-scale engineering analysis programs are among the most difficult to develop, maintain, and extend. The translation of a few pages of classical mathematics turns into tens of thousands of lines of nontrivial code. This paper discusses the role of data abstraction in engineering program development, where data, instead of processes, are used to decompose a program into parts. Data abstraction improves the modularity of a program by encapsulating implementation details and by providing a clear delineation between design and implementation. We describe a library of finite element data types that have been designed with data abstraction in mind. Using this approach, multiple representations and algorithms coexist, with proper selection made at run time. In addition, space-time trade-offs can generally be postponed without impacting other parts of the program. Throughout the paper, we address design issues with careful specifications of program behavior and implementation issues using object-oriented languages, which support data abstraction as well as polymorphism and inheritance.}, number={3}, journal={Journal of Computing in Civil Engineering}, author={Baugh, J.W. and Rehak, D.R.}, year={1992}, pages={282–301} }
 @article{using formal methods to specify the functional properties of engineering software_1992, volume={45}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0026940459&partnerID=MN8TOARS}, DOI={10.1016/0045-7949(92)90440-B}, abstractNote={Abstract This paper describes the use of formal methods in specifying the functional properties of engineering software components, an approach that enables one to deal more effectively with the complexities of large-scale engineering software systems. Because they are formal objects, these specifications can be manipulated using ordinary mathematics, validated with respect to formal requirements, and shown to satisfy properties such as consistency and completeness. In addition, their concise and unambiguous nature makes them suitable for both communication and commentary, which are not possible with substantial program texts. We present detailed examples of formally defined abstract data types, and discuss the role and potential benefits of formal specifications in engineering program design.}, number={3}, journal={Computers and Structures}, year={1992}, pages={557–570} }
 @inproceedings{program design with algebraic specifications_1991, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0025857871&partnerID=MN8TOARS}, year={1991}, pages={345–352} }
 @inproceedings{baugh_rehak_1989, title={Object-oriented design of finite element programs}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0024863017&partnerID=MN8TOARS}, author={Baugh, John W.Jr and Rehak, Daniel R.}, year={1989}, pages={91–100} }
 @article{rasdorf_ulberg_baugh_1987, title={A STRUCTURE-BASED MODEL OF SEMANTIC INTEGRITY CONSTRAINTS FOR RELATIONAL DATABASES}, volume={2}, ISSN={["0177-0667"]}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-0023120016&partnerID=MN8TOARS}, DOI={10.1007/BF01200175}, number={1}, journal={ENGINEERING WITH COMPUTERS}, author={RASDORF, WJ and ULBERG, KJ and BAUGH, JW}, year={1987}, pages={31–39} }