Object based software engineering with hidden sorted ECATNets and hidden labeled rewriting logic

Hidden sorted ECATNets and hidden labeled rewriting logic were introduced independently from each other. Hidden sorted ECATNets were developed to meet the objectives of object based software engineering. Their semantics in terms of logic of concurrency allows them to be used in the life cycle of sequential as well as concurrent and distributed systems. They are mainly useful in the earliest stages of the life cycle, i.e., for system requirements specification and validation through prototyping. Hidden labeled rewriting logic was introduced to deal with concurrent bisimulation, a concept that is essentially equivalent to observational equivalence useful for comparing different concurrent systems and proving their correctness. We first state under which conditions hidden sorted ECATNets may be interpreted in terms of hidden labeled rewriting logic, then we show how both formalisms may be associated for efficient prototyping and correct (or incorrect) refinement of system specification. Our exposition is illustrated by a known example from the area of communication protocols