SYNTHESIZING STATE-BASED OBJECT SYSTEMS FROM LSC SPECIFICATIONS

DOI10.1142/S0129054102000935MaRDI QIDQ3021937zbMATH OpenOpenAlexFDO

Authors David Harel, Hillel Kugler

Publication date 22 June 2005

Published in International Journal of Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1142/s0129054102000935

zbMATH Keywords

object-oriented systemsreactive systemssequence chartssoftware engineeringstatechartssynthesis

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1773071
• LSCs: Breathing life into message sequence charts
• FM 2005: Formal Methods
• Formal Methods in Software and Systems Modeling
• Synthesis from scenario-based specifications

Cites work

• A Deductive Approach to Program Synthesis
• Constructing Programs from Example Computations
• Statecharts: a visual formalism for complex systems
• Using branching time temporal logic to synthesize synchronization skeletons

Cited in

(17)

• GR(1)*: GR(1) specifications extended with existential guarantees
• The computational complexity of scenario-based agent verification and design
• Infinite-state high-level MSCs: model-checking and realizability
• State-bases approaches: from Z to Object-Z
• Composition of Use Cases Using Synchronization and Model Checking
• Automatic synthesis of SDL from MSC and its applications in forward and reverse engineering
• Synthesis from scenario-based specifications
• scientific article; zbMATH DE number 1773071 (Why is no real title available?)
• Statechartable Petri nets
• scientific article; zbMATH DE number 1870533 (Why is no real title available?)
• Synthesis of Reo circuits from scenario-based specifications
• On the power of play-out for scenario-based programs
• Synthesis of Reo circuits from scenario-based interaction specifications
• FM 2005: Formal Methods
• Live and let die: LSC-based verification of UML-models.
• Scenario-based verification of real-time systems using UPPAAL
• GR(1)*: GR(1) specifications extended with existential guarantees

This page was built for publication: SYNTHESIZING STATE-BASED OBJECT SYSTEMS FROM LSC SPECIFICATIONS

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3021937)