Trace-Directed Modeling - Polytechnique Montréal

Trace-Directed Modeling - Polytechnique Montréal

Trace-Directed Modelling State-of-the-Art, Ideas and Plans Timothy C. Lethbridge CRuiSE (Complexity Reduction in Software Engineering) Research Group SITE (School of Information Technology and Engineering) University of Ottawa December 2009 [email protected] http://www.site.uottawa.ca/~tcl Timothy C. Lethbridge Dec 2009 - 1 Agenda Current status

Quick overview of subproject intent State of the art Verification and analysis using state machines Reverse engineering from traces State machine generation and modeling Umple: A modeling infrastructure Plans and potential directions Timothy C. Lethbridge Dec 2009 - 2 Current Status Project considerably delayed due to difficulty recruiting students However I finally have three new students who are

supposed to be starting in January Two for this project and one for basic science that will help with this project Hamoud Aljamaan Ahmed and Mahmoud Orabi More later on plans Timothy C. Lethbridge Dec 2009 - 3 Agenda Current status Quick overview of subproject intent State of the art Verification and analysis using state machines

Reverse engineering from traces State machine generation and modeling Umple: A modeling infrastructure Plans and potential directions Timothy C. Lethbridge Dec 2009 - 4 Quick Overview of Subproject Intent Find ways to improve models so tracing can be more effectively performed Models that simplify understanding and design for multi-core architectures With adjustable levels of abstraction Generating an optimal set of tracepoints

Find better ways to extract models from traces Match traces to models they were generated from to increase understanding and find discrepancies It was previously agreed that the focus of modeling will be using large-scale concurrent state machines All the above is subject to adjustment according to the needs of the sponsors Timothy C. Lethbridge Dec 2009 - 5 Agenda Current status Quick overview of subproject intent State of the art Verification and analysis using state machines

Reverse engineering from traces State machine generation and modeling Umple: A modeling infrastructure Plans and potential directions Timothy C. Lethbridge Dec 2009 - 6 State of the Art - Verification Using State Machine Models - Li et. Al. Li, X., Qiu, X., Wang, L., Lei, B., and Wong, W. E. 2008. UML state machine diagram driven runtime verification of Java programs for message interaction consistency. Proc ACM SAC '08. pp 384-389. DOI= http://doi.acm.org/10.1145/1363686.1363781

Steps in their method Design the system with method call sequences specified using a state machine Instrument method calls to allow tracing Drive program with random test cases to generate traces Verify sequences match the original design Timothy C. Lethbridge Dec 2009 - 7 Sample State Machine Used in the Experiments of Li et. al.

Timothy C. Lethbridge Dec 2009 - 8 State of the art - Bottleneck Detection and Elimination - Saidi et al. Saidi, A. G., Binkert, N. L., Reinhardt, S. K., & Mudge, T. End-to-end performance forecasting: finding bottlenecks before they happen. Proc 36th Annual International Symposium on Computer Architecture, 2009. ISCA '09. ACM, pp.361-370. DOI= http://doi.acm.org/10.1145/1555754.1555800 Overall approach aims to analyse hardware+software in multi-core systems Identify end-to-end critical paths

Modelling performed as collections of state machines interacting via queues Case study: Linux TCP/IP stack & ethernet controller Identifies bottlenecks, then change model to remove Timothy C. Lethbridge Dec 2009 - 9 Saidi et al contd: Method Start with state machines if possible But if the system is not modelled with state machines then: Reverse engineer a state machine Little detail in this paper - I will discuss later Manually refine the state machine so it has the required level of abstraction

Convert multiple interacting state machines into a dependency graph Transitions become the nodes States become arc with timing while in state Timothy C. Lethbridge Dec 2009 - 10 Saidi et al contd: Sample Original State Machines Timothy C. Lethbridge Dec 2009 - 11 Saidi et al contd:

Sample Derived Dependency Graph Timothy C. Lethbridge Dec 2009 - 12 Saidi et al contd: Modifying Dependencies Timothy C. Lethbridge Dec 2009 - 13 Agenda Current status Quick overview of subproject intent

State of the art Verification and analysis using state machines Reverse engineering from traces State machine generation and modeling Umple: A modeling infrastructure Plans and potential directions Timothy C. Lethbridge Dec 2009 - 14 State of the art - Inferring Models from Traces - Walkinshaw et al Walkinshaw, N. and Bogdanov, K. Inferring Finite-State Models with Temporal Constraints. Proc 23rd IEEE/ACM international Conference on Automated Software Engineering 2008 pp. 248-257.

DOI= http://dx.doi.org/10.1109/ASE.2008.35 Key ideas State machine models have wide potential use They are unpopular due to weaknesses in tools to keep them up to date to generate them Reverse engineering complete state machines from traces is hard To generate a complete machine, complete path coverage needed A large number of test cases must be traced Temporal logic can help Timothy C. Lethbridge Dec 2009 - 15

Walkinshaw et al - contd: Literature Review Provides an excellent overview of the state of the art in inferring state machines from traces Traditional approach Passive merging of similar sequences in an augmented prefix tree acceptor (APTA) Exemplified in these papers A. Biermann and J. Feldman. On the synthesis of finite-state machines from samples of their behavior. IEEE Trans. Computers, 21:592597, 1972. G. Ammons, R. Bodk, and J. Larus. Mining specifications. POPL02, 416, 2002. J. E. Cook and A. L. Wolf. Discovering models of software processes from event-based data. ACM TOSEM, 7(3):215249, 1998. D. Lo and S. Khoo. SMArTIC: towards building an accurate, robust and scalable specification miner. In SIGSOFT FSE, 265275, 2006

Timothy C. Lethbridge Dec 2009 - 16 Walkinshaw et al - contd: The Evolution of State Merging Passive merging leads to overgeneralization if the traces dont cover the full space of possibilities A problem for most large systems without complete testcases More recent work: Active merging Asking questions of the developer when information is needed Exemplified in: P. Dupont, B. Lambeau, C. Damas, and A. van Lamsweerde. The QSM

algorithm and its application to software behavior model induction. Applied Artificial Intelligence, 22:77115, 2008. N. Walkinshaw, K. Bogdanov, M. Holcombe, and S. Salahuddin. Reverse engineering state machines by interactive grammar inference. WCRE07, 2007. Timothy C. Lethbridge Dec 2009 - 17 Walkinshaw et al - contd: Passive then Active Inference Timothy C. Lethbridge Dec 2009 - 18

Walkinshaw et al - contd: New approach uses LTL The developer suggests some constraints in Linear Temporal Logic An iterative process Timothy C. Lethbridge Dec 2009 - 19 LTL review Next x x has to hold in the next state Global x

x has to hold for every future state Eventually x x has to hold eventually Until x U y x has to hold until y Release x R y y is true until x becomes true x releases y You cant load again unless you close first Timothy C. Lethbridge Dec 2009 - 20 Walkinshaw et al: Sample Sequence of Reverse Engineering Steps

Timothy C. Lethbridge Dec 2009 - 21 Walkinshaw et al: Results Having the user be able to specify LTL constraints reduces the number of questions asked by 50-70% But: Reverse engineers must be fluent in temporal logic Maybe a better interaction method can be defined to allow LTL entry in a simpler form? Graphical? Patterns? System knowledge is still needed

Timothy C. Lethbridge Dec 2009 - 22 Agenda Current status Quick overview of subproject intent State of the art Verification and analysis using state machines Reverse engineering from traces State machine generation and modeling Umple: A modeling infrastructure Plans and potential directions Timothy C. Lethbridge

Dec 2009 - 23 State of the art: State Machine Modeling Tools and Code Generation Timothy C. Lethbridge Dec 2009 - 24 State of the art: URLs of Key State-Machine Generating Tools http://fsmgenerator.sourceforge.net/ http://www.smartstatestudio.com/ http://www.mentor.com/products/sm/model_developme nt/bridgepoint/

http://www.telelogic.se Timothy C. Lethbridge Dec 2009 - 25 Agenda Current status Quick overview of subproject intent State of the art Verification and analysis using state machines Reverse engineering from traces State machine generation and modeling Umple: A modeling infrastructure Plans and potential directions

Timothy C. Lethbridge Dec 2009 - 26 State of the Art: Umple, a Modeling Infrastructure Sponsored by IBM CAS Ottawa Project has one more year of current sponsorship A textual language in which UML concepts appear like programming language concepts Modelling can be performed Fully generated code that needs no round-tripping Programming can be done as normal Normal Java code, just incremented with UML abstractions Still under development, but robust enough for real development Current grammar is at:

http://cruise.site.uottawa.ca/umple/UmpleGrammar.html Timothy C. Lethbridge Dec 2009 - 27 Umple continued Associations: class X { } class Y { 1 -- * X; } Constraints maintained: Referential integrity Multiplicity

Umple is written in itself Online demo http://cruise.site.uottawa.ca/umpleonline/ Timothy C. Lethbridge Dec 2009 - 28 State Machines in Umple class X { SM1 { S1 { e1 / {callMethod();} -> S2;} S2 { e1 -> S1;} } } class Y {

Boolean b = true; SM2 { S3 { e2 [b] -> S4;} S4 { e3 -> / {setB(false);} S3;} } } Timothy C. Lethbridge Dec 2009 - 29 code class IntersectionTimerDriven { Integer directionOneGoTime;

Integer directionTwoGoTime; Integer yellowTime; Integer P1GoTime; Integer P2GoTime; flow { FourWayStop { entry / {directionOneLight = FlashingRed; directionTwoLight = FlashingRed; } initiateRegularOperation -> DirectionOneGo; } DirectionOneGo { entry / {directionOneLight = Green; directionTwoLight = Red; } afterSeconds(directionOneGoTime) -> DirectionOneHalting; detectMalfunction -> FourWayStop;

} DirectionOneHalting { entry / {directionOneLight = Yellow; } afterSeconds(yellowTime) -> DirectionTwoGo; detectMalfunction -> FourWayStop; } DirectionTwoGo { entry / {directionOneLight = Red; directionTwoLight = Green; } afterSeconds(directionTwoGoTime) -> DirectionTwoHalting; detectMalfunction -> FourWayStop; } DirectionTwoHalting { entry / {directionTwoLight = Yellow; } afterSeconds(yellowTime) -> DirectionOneGo;

detectMalfunction -> FourWayStop; } Timothy C. Lethbridge } pedestrianFlow { FourWayStop { entry / {P1Light = DoNotWalk; P2Light = DoNotWalk;} initiateRegularOperation -> P2Go; } P1Go { entry / {P1Light = Walk;} afterSeconds(P1GoTime) -> P1Halting; detectMalfunction -> FourWayStop; } P1halting {

entry / {P1Light = Flashing;} afterSeconds(P1GoTime) -> P2Go; detectMalfunction -> FourWayStop; } P2Go { entry / {P2Light = Walk;} afterSeconds(P2GoTime) -> P2Halting; detectMalfunction -> FourWayStop; } P2Halting { entry / {P2Light = Flashing;} afterSeconds(flashingTime) -> P1Go; detectMalfunction -> FourWayStop; }} directionOneLight { FlashingRed, Red, Yellow, Green

} directionTwoLight { FlashingRed, Red, Yellow, Green } P1Light { DoNotWalk, Flashing, Walk } P2Light { DoNotWalk. Flashing, Walk } Dec 2009 - 30 } Variability Modeling in Umple Allows Creating a product family

Putting together a product from sets of features http://cruise.site.uottawa.ca/umpleonline/vml.html Timothy C. Lethbridge Dec 2009 - 31 Why use Umple for this Project 1 Allows for Arbitrarily nested and concurrent states Interruptible do activities Multiple state machines per class Reusable state machines Product families of state machines Definition of model patterns Separation of diagrams from model

Aspects and mixins Timothy C. Lethbridge Dec 2009 - 32 Why use Umple for this Project 2 Integrated with Eclipse Works like any other compiler Generates multiple languages Under our control so we can experiment Textual So we can create, generate and edit sophisticated models easily So we can apply sophisticated tools to analyse and transform them But text is not XML, so merging and analysis can be easier

Graphical so we can visualize state machines Integrate state and class diagrams tightly Timothy C. Lethbridge Dec 2009 - 33 Agenda Current status Quick overview of subproject intent State of the art Verification and analysis using state machines Reverse engineering from traces State machine generation and modeling Umple: A modeling infrastructure Plans and potential directions

Timothy C. Lethbridge Dec 2009 - 34 Students to be Involved Directly on project (starting in January) Hamoud Aljamaan, PhD - Scholarship student Enhacing modeling tool Umple to facilitate tracing Mahmoud Orabi, PhD - Funded by project Reverse engineering traces to state machines Working on supporting technologies Ahmed Orabi, PhD student starting in January, NSERC funds Metamodeling for tracing Omar Badreldin, PhD student 30% completed, IBM funds State machine modeling and code generation

Andrew Forward, PhD student 90% completed, IBM funds Overall Umple architecture One more masters student is expected to start in May Also scholarships supported Making Umple generate for with C++ / Erlang, etc. Undergrad students working on IDE Timothy C. Lethbridge Dec 2009 - 35 Near-Term Plans: Develop and Enhance Tracable Models Manually model some existing systems of interest to Ericsson or DND Most effective do this in Umple If we have source code we can try re-factor to Umple

Refactor to associations and state machines Umple can be made to generate C++, Erlang, etc. We have a lot of experience refactoring to Umple with associations Learning to do it with state machines would be an interesting exercise Timothy C. Lethbridge Dec 2009 - 36 Near-term Plans: Reverse Enginering from Traces to State Machines Attempt to replicate (by borrowing software?) existing semi-automated reverse engineering techniques Target language would be Umple But easy to translate to and from other targets New research questions not addressed by current

research: Reverse engineering to concurrent state machines and nested state machines Full reverse engineering of correct guards, actions, and activities Can we make it work with truly huge traces? Timothy C. Lethbridge Dec 2009 - 37 Near-term plans: Deepen our literature review The new students who will be starting will be tasked with this Timothy C. Lethbridge

Dec 2009 - 38 Task for a student Work with Debrief software As provided by Mario Couture One of several case studies we will need to develop Instrument and trace Manually model prior to attempting to automatically model Generate code from the model for further experimentation Timothy C. Lethbridge Dec 2009 - 39

Other general project tasks Meet more with Ericsson and DND to better understand Perspectives Requirements Target examples Investigate synergies with IBM They are interested in Umple, but would like to see a customer interested in it before investing Timothy C. Lethbridge Dec 2009 - 40

Recently Viewed Presentations

  • Blueprint for Improved Results for Students with Disabilities

    Blueprint for Improved Results for Students with Disabilities

    Underlying Essential Understandings. Communities, boards of education, district and school leaders must provide systemic supports and professional development for teachers to meet the needs of students with disabilities, including appropriate identification and ensuring classrooms have necessary supports, rigorous and relevant...
  • Sub-brand to go here Doing gender through imagined

    Sub-brand to go here Doing gender through imagined

    155 words Working-class boy's essay misclassified as a girl's essay * I am married and I have no children. At the moment I am working in a pet shop. with all the animals arond me I am very fond of...
  • Graphic Communication Tutorial Booklet graphic communication @ st

    Graphic Communication Tutorial Booklet graphic communication @ st

    * Planometric - Interior View Stage three — wall units Add the positions of the wall units onto the floor plan as above. Project lines vertically as before. Mark the heights onto these line. You will need two sizes -...
  • The Brain - Use it or Lose it

    The Brain - Use it or Lose it

    The Brain - Use it or Lose it i cdnuolt blveiee that I clluod aulacity uesdnatnrd walht I was rdanieg. The phaonmeneal pweor of the hmuan mnid, aoccdrnig to rscheearch at Cmabridge Uinervtisy, it dseno't mtaetr in what oerdr the...
  • Technical Focus Mentoring programme Mentor training

    Technical Focus Mentoring programme Mentor training

    "There is somewhere out there I can go to" "I feel I am in control of my own career…the difference between before and now is huge!" "I have gained a trusting friend whose opinions I value" "Mentoring is not simply...
  • Geography of East Asia

    Geography of East Asia

    Physical Geography Continued. The physical makeup of East Asia has had a major impact on the history and development of each country.. The first settlers of . China. settled along major river systems such as the
  • American Realism (Regionalism & Naturalism)

    American Realism (Regionalism & Naturalism)

    American Realism (Regionalism & Naturalism)That man up there looks kind of scary; don't he? And don't look now, but how many points are on that pitchfork? And what does that pitchfork mean? It ain't really a pitchfork! 1860-1920. ... It's...
  • 1 Corinthians 12-16 - Brigham Young University-Idaho

    1 Corinthians 12-16 - Brigham Young University-Idaho

    1 Corinthians 12:1. JST, Concerning spiritual "things", I would not have you ignorant. Where the gifts of the Spirit are manifest, there is true religion; and where the gifts of the Spirit are not manifest, there true religion is not.