The paper presents an integrated approach to suspension design with educational purposes. A dedicated tool was created instruct automotive engineering students in the whole process of across various CAE tools involved, from early kinematics studies CAD, vehicle dynamics simulations and FEM modelling. has given birth a proven procedure that authors would like share this focus on side, although is not certainly novel subject itself. includes geometries widely used McPherson strut, complex...

Abstract The timed concurrent constraint language (tccp in short) is a logic based on the simple but powerful paradigm of Saraswat. In this paradigm, notion store-as-value replaced by store-as-constraint, which introduces some differences w.r.t. other approaches to concurrency. paper, we provide general framework for debugging tccp programs. To end, first present new compact, bottom-up semantics that well suited and verification purposes context reactive systems. We also an abstract allows...

In a UML model, different aspects of system are covered by types diagrams and this bears the risk that an overall specification becomes barely tractable designer. When model grows, it is likely architectural integrity will be compromised extensions bug-fixing operations. Hence, important to provide means help designers search in big models for particular instances some variable schema (design patterns) they construct. This can them both find potential problems architecture design ensure...

Achieving a quality software system requires UML designers to have good understanding of both design patterns and antipatterns. Unfortunately, models for real systems tend be huge hard manage, especially automatically generated from source code. Thus, it would advisable tools identify particular instances patterns. So, formal language express them is needed. However, textual formalization such barely usable by practitioners. In this paper we propose visual notation obtained adding as few...

This paper presents a technique to automatically infer algebraic property-oriented specifications from first-order Curry programs. is lazy functional logic language and the interaction between laziness logical variables raises some additional difficulties with respect other proposals for languages. Our statically infers source code of program specification which consists set equations relating (nested) operation calls that have same behavior. We propose (glass-box) semantic-based inference...

Abstract Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of classical approaches are based on browsing structure some form model (which represents behavior program) to check if a given specification is valid. This implies that part has be built, and sometimes needed fragment quite huge. In this work, we provide an alternative automatic decision method whether property, specified in linear temporal logic, valid w.r.t. tccp program. Our...

This paper is an overview of our results on the application abstract interpretation concepts to various problems related verification logic programs. These include systematic design semantics modeling proof methods and characterization assertions as domains.

This paper is an overview of our results on the application abstract interpretation concepts to derivation a verification method for logic programs. These include systematic design semantics modeling various proof methods and characterization assertions as domains. We first apply framework defined in [5] derive inductive sufficient conditions partial correctness. Then domain formalized domain. can therefore assertion based method. finally show two different languages: decidable language Horn...

This paper presents a "proof of concept" prototype which is an instance semantics-based technique to automatically infer algebraic property-oriented specifications from Term Rewriting Systems. Namely, given the source code TRS we specification consists set equations relating (nested) terms (operation calls) that rewrite, for all possible instantiations, same values.

In this paper we present a novel condensed narrowing-like semantics that contains the minimal information which is needed to describe compositionally all possible rewritings of term rewriting system. We provide its goal-dependent top-down definition and, more importantly, an equivalent goal-independent bottom-up fixpoint characterization. prove soundness and completeness w.r.t. small-step behavior for full class systems.