Browsing by Subject "Design seeding"

Now showing 1 - 1 of 1

A demonstration of applying alloy to mechanical synthesis of electromechanical systems
(2015-12) Liu, David Allen; Khurshid, Sarfraz; Garg, Vijay
Formal verification methods have traditionally been used in industry for proofs of functional correctness; more recent advances in their use have given rise to additional applications in new domains. Electromechanical systems such as automotive transmissions or robotics have relied heavily on software and mechanical modeling to operate and test the given design; modeling tools that support automated analysis such as Alloy allow formal analysis techniques to apply to this domain, and also enable synthesis. Specifically, Alloy provides a language and toolset that can abstractly represent and solve for real-world instances, which enable engineers to develop a deeper understanding of the systems they are building. This goal of the report is to demonstrate the potential of applying the Alloy toolset for modeling and analysis to assist in the synthesis and operational correctness of software-driven mechanical designs. A survey of literature has been included to demonstrate the foundation of concepts and previous research done in the area, spanning both formal verification and electromechanical design fields. The report also includes two small but illustrative case studies that attempt at mechanical synthesis (or design seeding) using Alloy, and report the abstraction methods and techniques that succeeded in demonstrating design synthesis efforts.